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 e. V -> ~P A e. _V )

Proof

Step Hyp Ref Expression
1 pweq 
 |-  ( x = A -> ~P x = ~P A )
2 1 eleq1d 
 |-  ( x = A -> ( ~P x e. _V <-> ~P A e. _V ) )
3 vpwex 
 |-  ~P x e. _V
4 2 3 vtoclg 
 |-  ( A e. V -> ~P A e. _V )