Theorem 0nn0

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

	Ref	Expression
Assertion	0nn0	$$⊢0\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢0=0$$
2		elnn0	$$⊢0\in {\mathbb{N}}_0\leftrightarrow \left(0\in \mathbb{N}\vee 0=0\right)$$
3	2	biimpri	$$⊢\left(0\in \mathbb{N}\vee 0=0\right)\to 0\in {\mathbb{N}}_0$$
4	3	olcs	$$⊢0=0\to 0\in {\mathbb{N}}_0$$
5	1 4	ax-mp	$$⊢0\in {\mathbb{N}}_0$$