Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ x ⊆ y, hypo.
03. 1, 2 ⊢ x ∈ {x | x ⊆ y}, comp_intro 1 2.
04. ⊢ power y = {x | x ⊆ y}, power_eq.
05. 1, 2 ⊢ x ∈ power y, eq_subst_rev 4 3, P u ↔ x ∈ u.
power_intro. ⊢ set x → x ⊆ y → x ∈ power y, subj_intro_ii 5.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.