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 12525
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 12524 . 2 class 0
2 cn 12264 . . 3 class
3 cc0 11158 . . . 4 class 0
43csn 4633 . . 3 class {0}
52, 4cun 3945 . 2 class (ℕ ∪ {0})
61, 5wceq 1534 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  12526  nnssnn0  12527  nn0ssre  12528  nn0sscn  12529  nn0ex  12530  dfn2  12537  nn0addcl  12559  nn0mulcl  12560  nn0ssz  12633  dvdsprmpweqnn  16887  cply1coe0bi  22293  m2cpminvid2lem  22747  pmatcollpw3fi1  22781  dfrtrcl4  43405  corcltrcl  43406  cotrclrcl  43409
  Copyright terms: Public domain W3C validator