Definition df-n0 12473

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 12472	. 2 class ℕ0
2		cn 12212	. . 3 class ℕ
3		cc0 11110	. . . 4 class 0
4	3	csn 4629	. . 3 class {0}
5	2, 4	cun 3947	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1542	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12474  nnssnn0  12475  nn0ssre  12476  nn0sscn  12477  nn0ex  12478  dfn2  12485  nn0addcl  12507  nn0mulcl  12508  nn0ssz  12581  dvdsprmpweqnn  16818  cply1coe0bi  21824  m2cpminvid2lem  22256  pmatcollpw3fi1  22290  dfrtrcl4  42489  corcltrcl  42490  cotrclrcl  42493