Metamath Proof Explorer

Theorem pwexr

Description: Converse of the Axiom of Power Sets. Note that it does not require ax-pow . (Contributed by NM, 11-Nov-2003)

Ref Expression
Assertion pwexr 
|- ( ~P A e. V -> A e. _V )

Proof

Step Hyp Ref Expression
1 unipw 
 |-  U. ~P A = A
2 uniexg 
 |-  ( ~P A e. V -> U. ~P A e. _V )
3 1 2 eqeltrrid 
 |-  ( ~P A e. V -> A e. _V )