Definition df-n0 12484

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 12483	. 2 class ℕ0
2		cn 12212	. . 3 class ℕ
3		cc0 11075	. . . 4 class 0
4	3	csn 4584	. . 3 class {0}
5	2, 4	cun 3904	. 2 class (ℕ ∪ {0})
6	1, 5	wceq 1562	1 wff ℕ0 = (ℕ ∪ {0})

This definition is referenced by:  elnn0  12485  nnssnn0  12486  nn0ssre  12487  nn0sscn  12488  nn0ex  12489  dfn2  12496  nn0addcl  12518  nn0mulcl  12519  nn0ssz  12593  dvdsprmpweqnn  16923  cply1coe0bi  22367  m2cpminvid2lem  22816  pmatcollpw3fi1  22850  dfrtrcl4  44319  corcltrcl  44320  cotrclrcl  44323