Theorem map_from_term

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. 2, 3 ⊢ y x ∈ Y, uq_bounded_elim 2 3.
05. 2, 3 ⊢ set (y x), set_intro 4.
06. 2 ⊢ x ∈ X → set (y x), subj_intro 5.
07. 2 ⊢ ∀x. x ∈ X → set (y x), uq_intro 6.
08. 1 ⊢ function f, fn_from_term 1.
09. 1, 2 ⊢ dom f = X, dom_from_term 1 7.
10. 1, 2 ⊢ rng f ⊆ Y, rng_from_term 1 2.
11. 1, 2 ⊢ map f X Y, map_intro 8 9 10.
map_from_term. ⊢ f = {t | ∃x. x ∈ X ∧ t = (x, y x)} →
  (∀x. x ∈ X → y x ∈ Y) → map f X Y, subj_intro_ii 11.

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