Metamath Proof Explorer

Theorem nn0ex

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004)

Ref Expression
Assertion nn0ex 
|- NN0 e. _V

Proof

Step Hyp Ref Expression
1 df-n0 
 |-  NN0 = ( NN u. { 0 } )
2 nnex 
 |-  NN e. _V
3 snex 
 |-  { 0 } e. _V
4 2 3 unex 
 |-  ( NN u. { 0 } ) e. _V
5 1 4 eqeltri 
 |-  NN0 e. _V