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	$$⊢A\in \mathrm{V}\leftrightarrow A\in 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		pwidg	$$⊢A\in \mathrm{V}\to A\in 𝒫A$$
2		elex	$$⊢A\in 𝒫A\to A\in \mathrm{V}$$
3	1 2	impbii	$$⊢A\in \mathrm{V}\leftrightarrow A\in 𝒫A$$