Metamath Proof Explorer

Theorem pwexg

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion pwexg A V 𝒫 A V


Step Hyp Ref Expression
1 pweq x = A 𝒫 x = 𝒫 A
2 1 eleq1d x = A 𝒫 x V 𝒫 A V
3 vpwex 𝒫 x V
4 2 3 vtoclg A V 𝒫 A V