MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1o Structured version   Visualization version   GIF version

Definition df-1o 8487
Description: Define the ordinal number 1. Definition 2.1 of [Schloeder] p. 4. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
df-1o 1o = suc ∅

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 8480 . 2 class 1o
2 c0 4322 . . 3 class
32csuc 6373 . 2 class suc ∅
41, 3wceq 1533 1 wff 1o = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  df1o2  8494  1on  8499  1onOLD  8500  ordgt0ge1  8514  oa1suc  8552  o2p2e4  8562  om1  8563  oe1  8565  oelim2  8616  nnecl  8634  1onnALT  8662  omabs  8672  nnm1  8673  0sdom1domALT  9267  brttrcl2  9744  ssttrcl  9745  ttrcltr  9746  ttrclss  9750  dmttrcl  9751  rnttrcl  9752  ttrclselem2  9756  ackbij1lem14  10263  aleph1  10601  cfpwsdom  10614  nlt1pi  10936  indpi  10937  hash1  14404  aleph1re  16230  sltval2  27640  sltsolem1  27659  nosepnelem  27663  nolt02o  27679  bday1s  27815  cuteq1  27817  om2noseqlt  28227  bnj168  34494  satfv1  35106  fmla1  35130  rankeq1o  35900  finxp1o  37004  finxpreclem4  37006  finxp00  37014  ordeldif1o  42833  onov0suclim  42847  omabs2  42905  tfsconcatb0  42917  nlim1NEW  43016  aleph1min  43131  clsk1indlem1  43619
  Copyright terms: Public domain W3C validator