Theorem nn0ssre

Description: Nonnegative integers are a subset of the reals. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	nn0ssre	$$⊢{\mathbb{N}}_0\subseteq ℝ$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2		nnssre	$$⊢\mathbb{N}\subseteq ℝ$$
3		0re	$$⊢0\in ℝ$$
4		snssi	$$⊢0\in ℝ\to \left\{0\right\}\subseteq ℝ$$
5	3 4	ax-mp	$$⊢\left\{0\right\}\subseteq ℝ$$
6	2 5	unssi	$$⊢\mathbb{N}\cup \left\{0\right\}\subseteq ℝ$$
7	1 6	eqsstri	$$⊢{\mathbb{N}}_0\subseteq ℝ$$