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 8094
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 8087 . 2 class 2o
2 c1o 8086 . . 3 class 1o
32csuc 6187 . 2 class suc 1o
41, 3wceq 1528 1 wff 2o = suc 1o
Colors of variables: wff setvar class
This definition is referenced by:  2on  8102  2oex  8103  2on0  8104  df2o3  8108  ondif2  8118  o1p1e2  8156  o2p2e4  8157  oneo  8197  2onn  8256  1one2o  8259  nnm2  8266  nnneo  8268  nneob  8269  enpr2d  8586  snnen2o  8696  1sdom2  8706  1sdom  8710  en2  8743  pm54.43  9418  en2eleq  9423  en2other2  9424  infxpenc  9433  infxpenc2  9437  dju1p1e2ALT  9589  fin1a2lem4  9814  cfpwsdom  9995  canthp1lem2  10064  pwxpndom2  10076  tsk2  10176  hash2  13756  f1otrspeq  18506  pmtrf  18514  pmtrmvd  18515  pmtrfinv  18520  efgmnvl  18771  isnzr2  19966  unidifsnel  30223  unidifsnne  30224  ex-sategoelel12  32572  sltval2  33061  nosgnn0  33063  sltsolem1  33078  nosepnelem  33082  nolt02o  33097  1oequni2o  34532  finxpreclem3  34557  finxpreclem4  34558  finxpsuclem  34561  finxp2o  34563  pw2f1ocnv  39514  pwfi2f1o  39576  clsk1indlem1  40275
  Copyright terms: Public domain W3C validator