Description: The set of nonnegative integers exists. (Contributed by NM, 18Jul2004)
Ref  Expression  

Assertion  nn0ex   NN0 e. _V 
Step  Hyp  Ref  Expression 

1  dfn0   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 