Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ u ∈ {x}, hypo.
03. 1, 2 ⊢ u = x, sg_elim 1 2.
04. ⊢ x ⊆ x, incl_refl.
05. 1 ⊢ x ∈ power x, power_intro 1 4.
06. 1, 2 ⊢ u ∈ power x, eq_subst_rev 3 5, P u ↔ u ∈ power x.
07. 1 ⊢ u ∈ {x} → u ∈ power x, subj_intro 6.
08. 1 ⊢ ∀u. u ∈ {x} → u ∈ power x, uq_intro 7.
09. 1 ⊢ {x} ⊆ power x, incl_intro 8.
sg_incl_in_power. ⊢ set x → {x} ⊆ power x, subj_intro 9.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.