Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 3 ⊢ y ∈ img {(a, b)} {a}, hypo.
04. 3 ⊢ ∃x. x ∈ {a} ∧ (x, y) ∈ {(a, b)}, img_elim 3.
05. 5 ⊢ x ∈ {a} ∧ (x, y) ∈ {(a, b)}, hypo.
06. 5 ⊢ (x, y) ∈ {(a, b)}, conj_elimr 5.
07. 1, 2 ⊢ set (a, b), set_pair 1 2.
08. 1, 2, 5 ⊢ (x, y) = (a, b), sg_elim 7 6.
09. 1, 2, 5 ⊢ (a, b) = (x, y), eq_symm 8.
10. 1, 2, 5 ⊢ a = x ∧ b = y, pair_property 1 2 9.
11. 1, 2, 5 ⊢ b = y, conj_elimr 10.
12. 1, 2, 5 ⊢ y = b, eq_symm 11.
13. 1, 2, 5 ⊢ y ∈ {b}, sg_intro 2 12.
14. 1, 2, 3 ⊢ y ∈ {b}, ex_elim 4 13.
15. 1, 2 ⊢ y ∈ img {(a, b)} {a} → y ∈ {b}, subj_intro 14.
16. 16 ⊢ y ∈ {b}, hypo.
17. 2, 16 ⊢ y = b, sg_elim 2 16.
18. ⊢ (a, b) = (a, b), eq_refl.
19. 2, 16 ⊢ (a, y) = (a, b), eq_subst_rev 17 18,
P u ↔ (a, u) = (a, b).
20. 1, 2, 16 ⊢ (a, y) ∈ {(a, b)}, sg_intro 7 19.
21. ⊢ a = a, eq_refl.
22. 1 ⊢ a ∈ {a}, sg_intro 1 21.
23. 1, 2, 16 ⊢ y ∈ img {(a, b)} {a}, img_intro 22 20.
24. 1, 2 ⊢ y ∈ {b} → y ∈ img {(a, b)} {a}, subj_intro 23.
25. 1, 2 ⊢ y ∈ img {(a, b)} {a} ↔ y ∈ {b}, bij_intro 15 24.
26. 1, 2 ⊢ ∀y. y ∈ img {(a, b)} {a} ↔ y ∈ {b}, uq_intro 25.
27. 1, 2 ⊢ img {(a, b)} {a} = {b}, ext 26.
img_sg_sg. ⊢ set a → set b → img {(a, b)} {a} = {b}, subj_intro_ii 27.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.