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 )