Metamath Proof Explorer

Theorem nn0rei

Description: A nonnegative integer is a real number. (Contributed by NM, 14-May-2003)

Ref Expression
Hypothesis nn0rei.1 
|- A e. NN0
Assertion nn0rei 
|- A e. RR

Proof

Step Hyp Ref Expression
1 nn0rei.1 
 |-  A e. NN0
2 nn0ssre 
 |-  NN0 C_ RR
3 2 1 sselii 
 |-  A e. RR