Definition df-n0

Description: Define the set of nonnegative integers. (Contributed by Raph Levien, 10-Dec-2002)

	Ref	Expression
Assertion	df-n0	$$⊢{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cn0	$$class{\mathbb{N}}_0$$
1		cn	$$class\mathbb{N}$$
2		cc0	$$class0$$
3	2	csn	$$class\left\{0\right\}$$
4	1 3	cun	$$class\left(\mathbb{N}\cup \left\{0\right\}\right)$$
5	0 4	wceq	$$wff{\mathbb{N}}_0=\mathbb{N}\cup \left\{0\right\}$$