Theorem map_rng_elim

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ y ∈ rng f, hypo.
03. 1 ⊢ img f X = rng f, map_img_of_dom_is_rng 1.
04. 1, 2 ⊢ y ∈ img f X, eq_subst_rev 3 2, P t ↔ y ∈ t.
05. 1, 2 ⊢ ∃x. x ∈ X ∧ (x, y) ∈ f, img_elim 4.
06. 6 ⊢ x ∈ X ∧ (x, y) ∈ f, hypo.
07. 6 ⊢ x ∈ X, conj_eliml 6.
08. 6 ⊢ (x, y) ∈ f, conj_elimr 6.
09. 1, 6 ⊢ y = app f x, map_app_intro 1 8.
10. 1, 6 ⊢ x ∈ X ∧ y = app f x, conj_intro 7 9.
11. 1, 6 ⊢ ∃x. x ∈ X ∧ y = app f x, ex_intro 10.
12. 1, 2 ⊢ ∃x. x ∈ X ∧ y = app f x, ex_elim 5 11.
map_rng_elim. ⊢ map f X Y → y ∈ rng f →
  ∃x. x ∈ X ∧ y = app f x, subj_intro_ii 12.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.