Definition df-n0 12576

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 12575	. 2 class ℕ0
2		cn 12304	. . 3 class ℕ
3		cc0 11171	. . . 4 class 0
4	3	csn 4583	. . 3 class {0}
5	2, 4	cun 3896	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1570	1 wff ℕ0 = (ℕ ∪ {0})

This definition is used by:  elnn0  12577  nnssnn0  12578  nn0ssre  12579  nn0sscn  12580  nn0ex  12581  dfn2  12588  nn0addcl  12610  nn0mulcl  12611  nn0ssz  12685  dvdsprmpweqnn  17024  cply1coe0bi  22581  m2cpminvid2lem  23033  pmatcollpw3fi1  23067  dfrtrcl4  44682  corcltrcl  44683  cotrclrcl  44686