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

Metamath Proof Explorer

Theorem nnnn0

Description: A positive integer is a nonnegative integer. (Contributed by NM, 9-May-2004)

		Ref	Expression
	Assertion	nnnn0	$⊢ A \in ℕ \to A \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		nnssnn0	$⊢ ℕ \subseteq ℕ_{0}$
2	1	sseli	$⊢ A \in ℕ \to A \in ℕ_{0}$