Definition df-n0 12406

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 12405	. 2 class ℕ0
2		cn 12149	. . 3 class ℕ
3		cc0 11030	. . . 4 class 0
4	3	csn 4581	. . 3 class {0}
5	2, 4	cun 3900	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1542	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12407  nnssnn0  12408  nn0ssre  12409  nn0sscn  12410  nn0ex  12411  dfn2  12418  nn0addcl  12440  nn0mulcl  12441  nn0ssz  12515  dvdsprmpweqnn  16817  cply1coe0bi  22250  m2cpminvid2lem  22702  pmatcollpw3fi1  22736  dfrtrcl4  44046  corcltrcl  44047  cotrclrcl  44050