Theorem elnn0

Description: Nonnegative integers expressed in terms of naturals and zero. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2	1	eleq2i	$$⊢A\in {\mathbb{N}}_0\leftrightarrow A\in \left(\mathbb{N}\cup \left\{0\right\}\right)$$
3		elun	$$⊢A\in \left(\mathbb{N}\cup \left\{0\right\}\right)\leftrightarrow \left(A\in \mathbb{N}\vee A\in \left\{0\right\}\right)$$
4		c0ex	$$⊢0\in \mathrm{V}$$
5	4	elsn2	$$⊢A\in \left\{0\right\}\leftrightarrow A=0$$
6	5	orbi2i	$$⊢\left(A\in \mathbb{N}\vee A\in \left\{0\right\}\right)\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
7	2 3 6	3bitri	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$