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 ⊆ ℤ