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 11751
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 11750 . 2 class 0
2 cn 11491 . . 3 class
3 cc0 10388 . . . 4 class 0
43csn 4476 . . 3 class {0}
52, 4cun 3861 . 2 class (ℕ ∪ {0})
61, 5wceq 1522 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11752  nnssnn0  11753  nn0ssre  11754  nn0sscn  11755  nn0ex  11756  dfn2  11763  nn0addcl  11785  nn0mulcl  11786  nn0ssz  11857  dvdsprmpweqnn  16055  cply1coe0bi  20156  m2cpminvid2lem  21051  pmatcollpw3fi1  21085  dfrtrcl4  39593  corcltrcl  39594  cotrclrcl  39597
  Copyright terms: Public domain W3C validator