Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 3 ⊢ (x, y1) ∈ {(a, b)}, hypo.
04. 4 ⊢ (x, y2) ∈ {(a, b)}, hypo.
05. 1, 2 ⊢ set (a, b), set_pair 1 2.
06. 1, 2, 3 ⊢ (x, y1) = (a, b), sg_elim 5 3.
07. 1, 2, 4 ⊢ (x, y2) = (a, b), sg_elim 5 4.
08. 1, 2, 3 ⊢ (a, b) = (x, y1), eq_symm 6.
09. 1, 2, 4 ⊢ (a, b) = (x, y2), eq_symm 7.
10. 1, 2, 3 ⊢ a = x ∧ b = y1, pair_property 1 2 8.
11. 1, 2, 4 ⊢ a = x ∧ b = y2, pair_property 1 2 9.
12. 1, 2, 3 ⊢ b = y1, conj_elimr 10.
13. 1, 2, 4 ⊢ b = y2, conj_elimr 11.
14. 1, 2, 3 ⊢ y1 = b, eq_symm 12.
15. 1, 2, 3, 4 ⊢ y1 = y2, eq_trans 14 13.
16. 1, 2 ⊢ (x, y1) ∈ {(a, b)} → (x, y2) ∈ {(a, b)} →
y1 = y2, subj_intro_ii 15.
17. 1, 2 ⊢ ∀y2. (x, y1) ∈ {(a, b)} → (x, y2) ∈ {(a, b)} →
y1 = y2, uq_intro 16.
18. 1, 2 ⊢ ∀y1. ∀y2. (x, y1) ∈ {(a, b)} → (x, y2) ∈ {(a, b)} →
y1 = y2, uq_intro 17.
19. 1, 2 ⊢ ∀x. ∀y1. ∀y2. (x, y1) ∈ {(a, b)} → (x, y2) ∈ {(a, b)} →
y1 = y2, uq_intro 18.
20. 1, 2 ⊢ relation {(a, b)}, sg_relation 1 2.
21. 1, 2 ⊢ function {(a, b)}, function_intro 20 19.
sg_function. ⊢ set a → set b → function {(a, b)}, subj_intro_ii 21.
Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, ext, lem, pairing, subset, union.