Theorem pwv

Description: The power class of the universe is the universe. Exercise 4.12(d) of Mendelson p. 235.

The collection of all classes is of course larger than _V , which is the collection of all sets. But ~PV , being a class, cannot contain proper classes, so ~P V is actually no larger than _V . This fact is exploited in ncanth . (Contributed by NM, 14-Sep-2003)

	Ref	Expression
Assertion	pwv	$$⊢𝒫\mathrm{V}=\mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢x\subseteq \mathrm{V}$$
2		velpw	$$⊢x\in 𝒫\mathrm{V}\leftrightarrow x\subseteq \mathrm{V}$$
3	1 2	mpbir	$$⊢x\in 𝒫\mathrm{V}$$
4		vex	$$⊢x\in \mathrm{V}$$
5	3 4	2th	$$⊢x\in 𝒫\mathrm{V}\leftrightarrow x\in \mathrm{V}$$
6	5	eqriv	$$⊢𝒫\mathrm{V}=\mathrm{V}$$