This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

Step Hyp Ref Expression
1 unipw ⊢ ⋃ 𝒫 A = A
2 uniexg ⊢ 𝒫 A ∈ V → ⋃ 𝒫 A ∈ V
3 1 2 eqeltrrid ⊢ 𝒫 A ∈ V → A ∈ V