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.
07. 1 ⊢ set {{x, y}}, setr_from_union 3.
08. 1 ⊢ set {x, y}, set_from_sg 7.
09. 1 ⊢ set {y}, setr_from_union 8.
10. 1 ⊢ set y, set_from_sg 9.
setr_from_pair. ⊢ set (x, y) → set y, subj_intro 10.
Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.