Metamath Proof Explorer


Theorem nn0ssz

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

Ref Expression
Assertion nn0ssz 0

Proof

Step Hyp Ref Expression
1 df-n0 0 = 0
2 nnssz
3 0z 0
4 c0ex 0 V
5 4 snss 0 0
6 3 5 mpbi 0
7 2 6 unssi 0
8 1 7 eqsstri 0