Definition df-n0 12527

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 12526	. 2 class ℕ0
2		cn 12266	. . 3 class ℕ
3		cc0 11155	. . . 4 class 0
4	3	csn 4626	. . 3 class {0}
5	2, 4	cun 3949	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12528  nnssnn0  12529  nn0ssre  12530  nn0sscn  12531  nn0ex  12532  dfn2  12539  nn0addcl  12561  nn0mulcl  12562  nn0ssz  12636  dvdsprmpweqnn  16923  cply1coe0bi  22306  m2cpminvid2lem  22760  pmatcollpw3fi1  22794  dfrtrcl4  43751  corcltrcl  43752  cotrclrcl  43755