Definition df-n0 12389

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 12388	. 2 class ℕ0
2		cn 12132	. . 3 class ℕ
3		cc0 11013	. . . 4 class 0
4	3	csn 4575	. . 3 class {0}
5	2, 4	cun 3896	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1541	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12390  nnssnn0  12391  nn0ssre  12392  nn0sscn  12393  nn0ex  12394  dfn2  12401  nn0addcl  12423  nn0mulcl  12424  nn0ssz  12498  dvdsprmpweqnn  16799  cply1coe0bi  22218  m2cpminvid2lem  22670  pmatcollpw3fi1  22704  dfrtrcl4  43855  corcltrcl  43856  cotrclrcl  43859