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

Metamath Proof Explorer

Theorem 0nn0

Description: 0 is a nonnegative integer. (Contributed by Raph Levien, 10-Dec-2002)

		Ref	Expression
	Assertion	0nn0	$⊢ 0 \in ℕ_{0}$

Step	Hyp	Ref	Expression
1		eqid	$⊢ 0 = 0$
2		elnn0	$⊢ 0 \in ℕ_{0} \leftrightarrow (0 \in ℕ \lor 0 = 0)$
3	2	biimpri	$⊢ (0 \in ℕ \lor 0 = 0) \to 0 \in ℕ_{0}$
4	3	olcs	$⊢ 0 = 0 \to 0 \in ℕ_{0}$
5	1 4	ax-mp	$⊢ 0 \in ℕ_{0}$