Proof
01. 1 ⊢ x ∈ power M, hypo.
02. ⊢ power M = {A | A ⊆ M}, power_eq.
03. 1 ⊢ x ∈ {A | A ⊆ M}, eq_subst 2 1, P u ↔ x ∈ u.
04. 1 ⊢ x ⊆ M, comp_elim 3.
power_elim. ⊢ x ∈ power M → x ⊆ M, subj_intro 4.
Dependencies
The given proof depends on two axioms:
comp, eq_subst.