Metamath Proof Explorer

Theorem nn0ssre

Description: Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002)

Ref Expression
Assertion nn0ssre 
|- NN0 C_ RR

Proof

Step Hyp Ref Expression
1 df-n0 
 |-  NN0 = ( NN u. { 0 } )
2 nnssre 
 |-  NN C_ RR
3 0re 
 |-  0 e. RR
4 snssi 
 |-  ( 0 e. RR -> { 0 } C_ RR )
5 3 4 ax-mp 
 |-  { 0 } C_ RR
6 2 5 unssi 
 |-  ( NN u. { 0 } ) C_ RR
7 1 6 eqsstri 
 |-  NN0 C_ RR