Metamath Proof Explorer

Theorem 0nn0

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Assertion 0nn0 
|- 0 e. NN0

Proof

Step Hyp Ref Expression
1 eqid 
 |-  0 = 0
2 elnn0 
 |-  ( 0 e. NN0 <-> ( 0 e. NN \/ 0 = 0 ) )
3 2 biimpri 
 |-  ( ( 0 e. NN \/ 0 = 0 ) -> 0 e. NN0 )
4 3 olcs 
 |-  ( 0 = 0 -> 0 e. NN0 )
5 1 4 ax-mp 
 |-  0 e. NN0