Metamath Proof Explorer

Theorem p0ex

Description: The power set of the empty set (the ordinal 1) is a set. See also p0exALT . (Contributed by NM, 23-Dec-1993)

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

Proof

Step Hyp Ref Expression
1 pw0 
 |-  ~P (/) = { (/) }
2 0ex 
 |-  (/) e. _V
3 2 pwex 
 |-  ~P (/) e. _V
4 1 3 eqeltrri 
 |-  { (/) } e. _V