Theorem pwexb

Description: The Axiom of Power Sets and its converse. A class is a set iff its power class is a set. (Contributed by NM, 11-Nov-2003)

	Ref	Expression
Assertion	pwexb	⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		pwexg	⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
2		pwexr	⊢ ( 𝒫 𝐴 ∈ V → 𝐴 ∈ V )
3	1 2	impbii	⊢ ( 𝐴 ∈ V ↔ 𝒫 𝐴 ∈ V )