Proof
01. 1 ⊢ set a, hypo.
02. 2 ⊢ set b, hypo.
03. 1, 2 ⊢ set (a, b), set_pair 1 2.
04. 4 ⊢ t ∈ {(a, b)}, hypo.
05. 1, 2, 4 ⊢ t = (a, b), sg_elim 3 4.
06. 1, 2, 4 ⊢ ∃y. t = (a, y), ex_intro 5.
07. 1, 2, 4 ⊢ ∃x. ∃y. t = (x, y), ex_intro 6.
08. 1, 2 ⊢ t ∈ {(a, b)} → ∃x. ∃y. t = (x, y), subj_intro 7.
09. 1, 2 ⊢ ∀t. t ∈ {(a, b)} → ∃x. ∃y. t = (x, y), uq_intro 8.
10. 1, 2 ⊢ relation {(a, b)}, relation_fold 9.
sg_relation. ⊢ set a → set b → relation {(a, b)}, subj_intro_ii 10.
Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, ext, pairing, union.