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 𝒫 A V A V


Step Hyp Ref Expression
1 unipw 𝒫 A = A
2 uniexg 𝒫 A V 𝒫 A V
3 1 2 eqeltrrid 𝒫 A V A V