Definition df-n0 12607

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 12606	. 2 class ℕ0
2		cn 12335	. . 3 class ℕ
3		cc0 11200	. . . 4 class 0
4	3	csn 4583	. . 3 class {0}
5	2, 4	cun 4149	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1569	1 wff ℕ0 = (ℕ ∪ {0})

This definition is used by:  elnn0  12608  nnssnn0  12609  nn0ssre  12610  nn0sscn  12611  nn0ex  12612  dfn2  12619  nn0addcl  12641  nn0mulcl  12642  nn0ssz  12716  dvdsprmpweqnn  17063  cply1coe0bi  22620  m2cpminvid2lem  23072  pmatcollpw3fi1  23106  dfrtrcl4  44780  corcltrcl  44781  cotrclrcl  44784