Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 3 ⊢ x ∈ dom {(a, b)}, hypo.
04. 3 ⊢ ∃y. (x, y) ∈ {(a, b)}, dom_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 ⊢ a = x, conj_eliml 9.
11. 1, 2, 5 ⊢ x = a, eq_symm 10.
12. 1, 2, 3 ⊢ x = a, ex_elim 4 11.
13. 1, 2, 3 ⊢ x ∈ {a}, sg_intro 1 12.
14. 1, 2 ⊢ x ∈ dom {(a, b)} → x ∈ {a}, subj_intro 13.
15. 15 ⊢ x ∈ {a}, hypo.
16. 1, 15 ⊢ x = a, sg_elim 1 15.
17. ⊢ (a, b) = (a, b), eq_refl.
18. 1, 15 ⊢ (x, b) = (a, b), eq_subst_rev 16 17, P u ↔ (u, b) = (a, b).
19. 1, 2, 15 ⊢ (x, b) ∈ {(a, b)}, sg_intro 6 18.
20. 1, 2, 15 ⊢ x ∈ dom {(a, b)}, dom_intro 19.
21. 1, 2 ⊢ x ∈ {a} → x ∈ dom {(a, b)}, subj_intro 20.
22. 1, 2 ⊢ x ∈ dom {(a, b)} ↔ x ∈ {a}, bij_intro 14 21.
23. 1, 2 ⊢ ∀x. x ∈ dom {(a, b)} ↔ x ∈ {a}, uq_intro 22.
24. 1, 2 ⊢ dom {(a, b)} = {a}, ext 23.
dom_sg. ⊢ set a → set b → dom {(a, b)} = {a}, subj_intro_ii 24.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.