Theorem map_app_in_cod

Proof
01. 1 ⊢ map f X Y, hypo.
02. 2 ⊢ x ∈ X, hypo.
03. 1, 2 ⊢ ∃y. y ∈ Y ∧ y = app f x, map_app_exists 1 2.
04. 4 ⊢ y ∈ Y ∧ y = app f x, hypo.
05. 4 ⊢ y ∈ Y, conj_eliml 4.
06. 4 ⊢ y = app f x, conj_elimr 4.
08. 4 ⊢ app f x ∈ Y, eq_subst 6 5, P u ↔ u ∈ Y.
09. 1, 2 ⊢ app f x ∈ Y, ex_elim 3 8.
map_app_in_cod. ⊢ map f X Y → x ∈ X → app f x ∈ Y, subj_intro_ii 9.

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