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 )