Metamath Proof Explorer


Theorem pp0ex

Description: The power set of the power set of the empty set (the ordinal 2) is a set. (Contributed by NM, 24-Jun-1993)

Ref Expression
Assertion pp0ex
|- { (/) , { (/) } } e. _V

Proof

Step Hyp Ref Expression
1 pwpw0
 |-  ~P { (/) } = { (/) , { (/) } }
2 p0ex
 |-  { (/) } e. _V
3 2 pwex
 |-  ~P { (/) } e. _V
4 1 3 eqeltrri
 |-  { (/) , { (/) } } e. _V