Theorem pwidb

Description: A class is an element of its powerclass if and only if it is a set. (Contributed by BJ, 31-Dec-2023)

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

Proof

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