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 ( 𝒫 𝐴𝑉𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 unipw 𝒫 𝐴 = 𝐴
2 uniexg ( 𝒫 𝐴𝑉 𝒫 𝐴 ∈ V )
3 1 2 eqeltrrid ( 𝒫 𝐴𝑉𝐴 ∈ V )