Definition df-n0 12427

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 12426	. 2 class ℕ0
2		cn 12163	. . 3 class ℕ
3		cc0 11027	. . . 4 class 0
4	3	csn 4557	. . 3 class {0}
5	2, 4	cun 3883	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1542	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12428  nnssnn0  12429  nn0ssre  12430  nn0sscn  12431  nn0ex  12432  dfn2  12439  nn0addcl  12461  nn0mulcl  12462  nn0ssz  12536  dvdsprmpweqnn  16845  cply1coe0bi  22255  m2cpminvid2lem  22707  pmatcollpw3fi1  22741  dfrtrcl4  44153  corcltrcl  44154  cotrclrcl  44157