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