Metamath Proof Explorer

Theorem pwexb

Description: The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion pwexb 
|- ( A e. _V <-> ~P A e. _V )

Proof

Step Hyp Ref Expression
1 pwexg 
 |-  ( A e. _V -> ~P A e. _V )
2 pwexr 
 |-  ( ~P A e. _V -> A e. _V )
3 1 2 impbii 
 |-  ( A e. _V <-> ~P A e. _V )