Definition df-n0 12504

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 12503	. 2 class ℕ0
2		cn 12232	. . 3 class ℕ
3		cc0 11099	. . . 4 class 0
4	3	csn 4588	. . 3 class {0}
5	2, 4	cun 3902	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1568	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12505  nnssnn0  12506  nn0ssre  12507  nn0sscn  12508  nn0ex  12509  dfn2  12516  nn0addcl  12538  nn0mulcl  12539  nn0ssz  12613  dvdsprmpweqnn  16944  cply1coe0bi  22441  m2cpminvid2lem  22890  pmatcollpw3fi1  22924  dfrtrcl4  44412  corcltrcl  44413  cotrclrcl  44416