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