MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-n0 Structured version   Visualization version   GIF version

Definition df-n0 12470
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
StepHypRef Expression
1 cn0 12469 . 2 class 0
2 cn 12209 . . 3 class
3 cc0 11107 . . . 4 class 0
43csn 4628 . . 3 class {0}
52, 4cun 3946 . 2 class (ℕ ∪ {0})
61, 5wceq 1542 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  12471  nnssnn0  12472  nn0ssre  12473  nn0sscn  12474  nn0ex  12475  dfn2  12482  nn0addcl  12504  nn0mulcl  12505  nn0ssz  12578  dvdsprmpweqnn  16815  cply1coe0bi  21816  m2cpminvid2lem  22248  pmatcollpw3fi1  22282  dfrtrcl4  42475  corcltrcl  42476  cotrclrcl  42479
  Copyright terms: Public domain W3C validator