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 8093
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
df-1o 1o = suc ∅

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 8086 . 2 class 1o
2 c0 4290 . . 3 class
32csuc 6187 . 2 class suc ∅
41, 3wceq 1528 1 wff 1o = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  8100  df1o2  8107  ordgt0ge1  8113  oa1suc  8147  om1  8158  oe1  8160  oelim2  8211  nnecl  8229  1onn  8255  omabs  8264  nnm1  8265  0sdom1dom  8705  ackbij1lem14  9644  aleph1  9982  cfpwsdom  9995  nlt1pi  10317  indpi  10318  hash1  13755  aleph1re  15588  bnj168  31900  satfv1  32508  fmla1  32532  sltval2  33061  sltsolem1  33078  nosepnelem  33082  nolt02o  33097  rankeq1o  33530  finxp1o  34556  finxpreclem4  34558  finxp00  34566  aleph1min  39796  clsk1indlem1  40275
  Copyright terms: Public domain W3C validator