Metamath Proof Explorer

Theorem pwex

Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis pwex.1 
|- A e. _V
Assertion pwex 
|- ~P A e. _V

Proof

Step Hyp Ref Expression
1 pwex.1 
 |-  A e. _V
2 pwexg 
 |-  ( A e. _V -> ~P A e. _V )
3 1 2 ax-mp 
 |-  ~P A e. _V