Metamath Proof Explorer

Theorem nn0ssz

Description: Nonnegative integers are a subset of the integers. (Contributed by NM, 9-May-2004)

Ref Expression
Assertion nn0ssz 
|- NN0 C_ ZZ

Proof

Step Hyp Ref Expression
1 df-n0 
 |-  NN0 = ( NN u. { 0 } )
2 nnssz 
 |-  NN C_ ZZ
3 0z 
 |-  0 e. ZZ
4 c0ex 
 |-  0 e. _V
5 4 snss 
 |-  ( 0 e. ZZ <-> { 0 } C_ ZZ )
6 3 5 mpbi 
 |-  { 0 } C_ ZZ
7 2 6 unssi 
 |-  ( NN u. { 0 } ) C_ ZZ
8 1 7 eqsstri 
 |-  NN0 C_ ZZ