Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ set y, hypo.
03. 1 ⊢ set {x}, set_sg 1.
04. 1 ⊢ set {{x}}, set_sg 3.
05. 1, 2 ⊢ set {x, y}, pairing 1 2.
06. 1, 2 ⊢ set {{x, y}}, set_sg 5.
07. 1, 2 ⊢ set {{x}, {x, y}}, set_union 4 6.
08. 1, 2 ⊢ set (x, y), eq_subst_rev pair_eq 7, P u ↔ set u.
set_pair. ⊢ set x → set y → set (x, y), subj_intro_ii 8.
Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, ext, pairing, union.