Metamath Proof Explorer


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 𝒫 V = V

Proof

Step Hyp Ref Expression
1 ssv 𝑥 ⊆ V
2 velpw ( 𝑥 ∈ 𝒫 V ↔ 𝑥 ⊆ V )
3 1 2 mpbir 𝑥 ∈ 𝒫 V
4 vex 𝑥 ∈ V
5 3 4 2th ( 𝑥 ∈ 𝒫 V ↔ 𝑥 ∈ V )
6 5 eqriv 𝒫 V = V