Proof
01. 1 ⊢ set (x, y), hypo.
02. ⊢ (x, y) = {{x}, {x, y}}, pair_eq.
03. 1 ⊢ set {{x}, {x, y}}, eq_subst 2 1, P u ↔ set u.
04. 1 ⊢ set {{x}}, setl_from_union 3.
05. 1 ⊢ set {x}, set_from_sg 4.
06. 1 ⊢ set x, set_from_sg 5.
setl_from_pair. ⊢ set (x, y) → set x, subj_intro 6.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.