Theorem pwex

Description: Power set axiom expressed in class notation. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Hypothesis	pwex.1	⊢ 𝐴 ∈ V
Assertion	pwex	⊢ 𝒫 𝐴 ∈ V

Proof

Step	Hyp	Ref	Expression
1		pwex.1	⊢ 𝐴 ∈ V
2		pwexg	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
3	1 2	ax-mp	⊢ 𝒫 𝐴 ∈ V