Proof
01. 1 ⊢ set x, hypo.
02. 1 ⊢ set {x, x}, pairing 1 1.
03. ⊢ {x, x} = {x}, union_idem.
04. 1 ⊢ set {x}, eq_subst 3 2, P u ↔ set u.
set_sg. ⊢ set x → set {x}, subj_intro 4.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, pairing.