Definition df-n0 12450

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 12449	. 2 class ℕ0
2		cn 12193	. . 3 class ℕ
3		cc0 11075	. . . 4 class 0
4	3	csn 4592	. . 3 class {0}
5	2, 4	cun 3915	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1540	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12451  nnssnn0  12452  nn0ssre  12453  nn0sscn  12454  nn0ex  12455  dfn2  12462  nn0addcl  12484  nn0mulcl  12485  nn0ssz  12559  dvdsprmpweqnn  16863  cply1coe0bi  22196  m2cpminvid2lem  22648  pmatcollpw3fi1  22682  dfrtrcl4  43734  corcltrcl  43735  cotrclrcl  43738