This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnssnn0

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

		Ref	Expression
	Assertion	nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$

Step	Hyp	Ref	Expression
1		ssun1	$⊢ ℕ \subseteq ℕ \cup \{0\}$
2		df-n0	$⊢ ℕ_{0} = ℕ \cup \{0\}$
3	1 2	sseqtrri	$⊢ ℕ \subseteq ℕ_{0}$