Theorem map_from_term_app

Proof
01. 1 ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)}, hypo.
02. 2 ⊢ ∀x. x ∈ X → y x ∈ Y, hypo.
03. 3 ⊢ x ∈ X, hypo.
04. 1, 2 ⊢ map f X Y, map_from_term 1 2.
05. 2, 3 ⊢ y x ∈ Y, uq_bounded_elim 2 3.
06. 2, 3 ⊢ set (y x), set_intro 5.
07. 3 ⊢ set x, set_intro 3.
08. 2, 3 ⊢ set (x, y x), set_pair 7 6.
09. ⊢ (x, y x) = (x, y x), eq_refl.
10. 3 ⊢ x ∈ X ∧ (x, y x) = (x, y x), conj_intro 3 9.
12. 3 ⊢ ∃a. a ∈ X ∧ (x, y x) = (a, y a), ex_intro 10.
13. 2, 3 ⊢ (x, y x) ∈ {t | ∃a. a ∈ X ∧ t = (a, y a)},
  comp_intro 8 12, P t ↔ (∃a. a ∈ X ∧ t = (a, y a)).
14. 1, 2, 3 ⊢ (x, y x) ∈ f, eq_subst_rev 1 13, P u ↔ (x, y x) ∈ u.
15. 1, 2, 3 ⊢ y x = app f x, map_app_intro 4 14.
16. 1, 2, 3 ⊢ app f x = y x, eq_symm 15.
map_from_term_app. ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)} →
  (∀x. x ∈ X → y x ∈ Y) → x ∈ X → app f x = y x,
  subj_intro_iii 16.

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