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