Definition df-n0 12435

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 12434	. 2 class ℕ0
2		cn 12171	. . 3 class ℕ
3		cc0 11035	. . . 4 class 0
4	3	csn 4568	. . 3 class {0}
5	2, 4	cun 3888	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1542	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12436  nnssnn0  12437  nn0ssre  12438  nn0sscn  12439  nn0ex  12440  dfn2  12447  nn0addcl  12469  nn0mulcl  12470  nn0ssz  12544  dvdsprmpweqnn  16853  cply1coe0bi  22264  m2cpminvid2lem  22716  pmatcollpw3fi1  22750  dfrtrcl4  44162  corcltrcl  44163  cotrclrcl  44166