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 12524
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 12523 . 2 class 0
2 cn 12263 . . 3 class
3 cc0 11152 . . . 4 class 0
43csn 4630 . . 3 class {0}
52, 4cun 3960 . 2 class (ℕ ∪ {0})
61, 5wceq 1536 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  12525  nnssnn0  12526  nn0ssre  12527  nn0sscn  12528  nn0ex  12529  dfn2  12536  nn0addcl  12558  nn0mulcl  12559  nn0ssz  12633  dvdsprmpweqnn  16918  cply1coe0bi  22321  m2cpminvid2lem  22775  pmatcollpw3fi1  22809  dfrtrcl4  43727  corcltrcl  43728  cotrclrcl  43731
  Copyright terms: Public domain W3C validator