Proof
01. 1 ⊢ set X, hypo.
02. ⊢ {x | x ∈ X ∧ P x} ⊆ X, sep_is_subclass.
03. 1 ⊢ set {x | x ∈ X ∧ P x}, subset 2 1.
04. 1 ⊢ {x | x ∈ X ∧ P x} ∈ power X, power_intro 3 2.
sep_in_power. ⊢ set X → {x | x ∈ X ∧ P x} ∈ power X, subj_intro 4.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, subset.