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