Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ b ∈ Y, hypo.
03. 2 ⊢ set b, set_intro 2.
04. 1, 2 ⊢ function {(a, b)}, sg_function 1 3.
05. 1, 2 ⊢ dom {(a, b)} = {a}, dom_sg 1 3.
06. 1, 2 ⊢ rng {(a, b)} = {b}, rng_sg 1 3.
07. 1, 2 ⊢ rng {(a, b)} ⊆ {b}, incl_from_eq 6.
08. 2 ⊢ {b} ⊆ Y, sg_incl_in 2.
09. 1, 2 ⊢ rng {(a, b)} ⊆ Y, incl_trans 7 8.
10. 1, 2 ⊢ map {(a, b)} {a} Y, map_intro 4 5 9.
sg_map. ⊢ set a → b ∈ Y → map {(a, b)} {a} Y, subj_intro_ii 10.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.