Theorem nn0ex

Description: The set of nonnegative integers exists. (Contributed by NM, 18-Jul-2004)

	Ref	Expression
Assertion	nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$
2		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
3		snex	$$⊢\left\{0\right\}\in \mathrm{V}$$
4	2 3	unex	$$⊢\mathbb{N}\cup \left\{0\right\}\in \mathrm{V}$$
5	1 4	eqeltri	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$