Theorem nnssnn0

Description: Positive naturals are a subset of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	nnssnn0	⊢ ℕ ⊆ ℕ0

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ ℕ ⊆ ( ℕ ∪ { 0 } )
2		df-n0	⊢ ℕ0 = ( ℕ ∪ { 0 } )
3	1 2	sseqtrri	⊢ ℕ ⊆ ℕ0