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

Definition df-2o 8090
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
df-2o 2o = suc 1o

Detailed syntax breakdown of Definition df-2o
StepHypRef Expression
1 c2o 8083 . 2 class 2o
2 c1o 8082 . . 3 class 1o
32csuc 6165 . 2 class suc 1o
41, 3wceq 1538 1 wff 2o = suc 1o
Colors of variables: wff setvar class
This definition is referenced by:  2on  8098  2oex  8099  2on0  8100  df2o3  8104  ondif2  8114  o1p1e2  8152  o2p2e4  8153  o2p2e4OLD  8154  oneo  8194  2onn  8253  1one2o  8256  nnm2  8263  nnneo  8265  nneob  8266  enpr2d  8584  snnen2o  8695  1sdom2  8705  1sdom  8709  en2  8742  pm54.43  9418  en2eleq  9423  en2other2  9424  infxpenc  9433  infxpenc2  9437  dju1p1e2ALT  9589  fin1a2lem4  9818  cfpwsdom  9999  canthp1lem2  10068  pwxpndom2  10080  tsk2  10180  hash2  13766  f1otrspeq  18571  pmtrf  18579  pmtrmvd  18580  pmtrfinv  18585  efgmnvl  18836  isnzr2  20033  unidifsnel  30311  unidifsnne  30312  ex-sategoelel12  32788  sltval2  33277  nosgnn0  33279  sltsolem1  33294  nosepnelem  33298  nolt02o  33313  1oequni2o  34786  finxpreclem3  34811  finxpreclem4  34812  finxpsuclem  34815  finxp2o  34817  pw2f1ocnv  39971  pwfi2f1o  40033  clsk1indlem1  40741
  Copyright terms: Public domain W3C validator