Theorem nn0ssz

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

	Ref	Expression
Assertion	nn0ssz	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2		nnssz	$$⊢\mathbb{N}\subseteq \mathbb{Z}$$
3		0z	$$⊢0\in \mathbb{Z}$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	snss	$$⊢0\in \mathbb{Z}\leftrightarrow \left\{0\right\}\subseteq \mathbb{Z}$$
6	3 5	mpbi	$$⊢\left\{0\right\}\subseteq \mathbb{Z}$$
7	2 6	unssi	$$⊢\mathbb{N}\cup \left\{0\right\}\subseteq \mathbb{Z}$$
8	1 7	eqsstri	$$⊢{\mathbb{N}}_0\subseteq \mathbb{Z}$$