Theorem map_app_exists

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 1 ⊢ function f ∧ dom f = X ∧ rng f ⊆ Y, map_unfold 1.
04. 1 ⊢ function f ∧ dom f = X, conj_eliml 3.
05. 1 ⊢ function f, conj_eliml 4.
06. 1 ⊢ dom f = X, conj_elimr 4.
07. 1, 2 ⊢ x ∈ dom f, eq_subst_rev 6 2, P u ↔ x ∈ u.
08. 1, 2 ⊢ ∃y. y ∈ rng f ∧ y = app f x, fn_app_exists 5 7.
09. 9 ⊢ y ∈ rng f ∧ y = app f x, hypo.
10. 9 ⊢ y ∈ rng f, conj_eliml 9.
11. 1 ⊢ rng f ⊆ Y, conj_elimr 3.
12. 1, 9 ⊢ y ∈ Y, incl_elim 11 10.
13. 9 ⊢ y = app f x, conj_elimr 9.
14. 1, 9 ⊢ y ∈ Y ∧ y = app f x, conj_intro 12 13.
15. 1, 9 ⊢ ∃y. y ∈ Y ∧ y = app f x, ex_intro 14.
16. 1, 2 ⊢ ∃y. y ∈ Y ∧ y = app f x, ex_elim 8 15.
map_app_exists. ⊢ map f X Y → x ∈ X → ∃y. y ∈ Y ∧ y = app f x,
  subj_intro_ii 16.

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