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 0

Proof

Step Hyp Ref Expression
1 df-n0 0 = 0
2 nnssre
3 0re 0
4 snssi 0 0
5 3 4 ax-mp 0
6 2 5 unssi 0
7 1 6 eqsstri 0