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 11890
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 11889 . 2 class 0
2 cn 11629 . . 3 class
3 cc0 10530 . . . 4 class 0
43csn 4528 . . 3 class {0}
52, 4cun 3882 . 2 class (ℕ ∪ {0})
61, 5wceq 1538 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  11891  nnssnn0  11892  nn0ssre  11893  nn0sscn  11894  nn0ex  11895  dfn2  11902  nn0addcl  11924  nn0mulcl  11925  nn0ssz  11995  dvdsprmpweqnn  16215  cply1coe0bi  20933  m2cpminvid2lem  21363  pmatcollpw3fi1  21397  dfrtrcl4  40436  corcltrcl  40437  cotrclrcl  40440
  Copyright terms: Public domain W3C validator