Definition df-n0 12243

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 12242	. 2 class ℕ0
2		cn 11982	. . 3 class ℕ
3		cc0 10880	. . . 4 class 0
4	3	csn 4562	. . 3 class {0}
5	2, 4	cun 3886	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1539	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12244  nnssnn0  12245  nn0ssre  12246  nn0sscn  12247  nn0ex  12248  dfn2  12255  nn0addcl  12277  nn0mulcl  12278  nn0ssz  12350  dvdsprmpweqnn  16595  cply1coe0bi  21480  m2cpminvid2lem  21912  pmatcollpw3fi1  21946  dfrtrcl4  41353  corcltrcl  41354  cotrclrcl  41357