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

Metamath Proof Explorer

Theorem pwexg

Description: Power set axiom expressed in class notation, with the sethood requirement as an antecedent. (Contributed by NM, 30-Oct-2003)

Ref Expression
Assertion pwexg ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )

Proof

Step Hyp Ref Expression
1 pweq ⊢ ( 𝑥 = 𝐴 → 𝒫 𝑥 = 𝒫 𝐴 )
2 1 eleq1d ⊢ ( 𝑥 = 𝐴 → ( 𝒫 𝑥 ∈ V ↔ 𝒫 𝐴 ∈ V ) )
3 vpwex ⊢ 𝒫 𝑥 ∈ V
4 2 3 vtoclg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )