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 12372
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 12371 . 2 class 0
2 cn 12111 . . 3 class
3 cc0 11009 . . . 4 class 0
43csn 4584 . . 3 class {0}
52, 4cun 3906 . 2 class (ℕ ∪ {0})
61, 5wceq 1541 1 wff 0 = (ℕ ∪ {0})
Colors of variables: wff setvar class
This definition is referenced by:  elnn0  12373  nnssnn0  12374  nn0ssre  12375  nn0sscn  12376  nn0ex  12377  dfn2  12384  nn0addcl  12406  nn0mulcl  12407  nn0ssz  12480  dvdsprmpweqnn  16717  cply1coe0bi  21623  m2cpminvid2lem  22055  pmatcollpw3fi1  22089  dfrtrcl4  41921  corcltrcl  41922  cotrclrcl  41925
  Copyright terms: Public domain W3C validator