Metamath Proof Explorer

Definition df-n0

Description: Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Assertion df-n0 
|- NN0 = ( NN u. { 0 } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cn0 
 |-  NN0
1 cn 
 |-  NN
2 cc0 
 |-  0
3 2 csn 
 |-  { 0 }
4 1 3 cun 
 |-  ( NN u. { 0 } )
5 0 4 wceq 
 |-  NN0 = ( NN u. { 0 } )