Definition df-n0 12500

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

Assertion

Ref	Expression
df-n0	⊢ ℕ0 = (ℕ ∪ {0})

Detailed syntax breakdown of Definition df-n0

Step	Hyp	Ref	Expression
1		cn0 12499	. 2 class ℕ0
2		cn 12238	. . 3 class ℕ
3		cc0 11127	. . . 4 class 0
4	3	csn 4601	. . 3 class {0}
5	2, 4	cun 3924	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12501  nnssnn0  12502  nn0ssre  12503  nn0sscn  12504  nn0ex  12505  dfn2  12512  nn0addcl  12534  nn0mulcl  12535  nn0ssz  12609  dvdsprmpweqnn  16903  cply1coe0bi  22238  m2cpminvid2lem  22690  pmatcollpw3fi1  22724  dfrtrcl4  43709  corcltrcl  43710  cotrclrcl  43713