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 7448
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
df-2o 2𝑜 = suc 1𝑜

Detailed syntax breakdown of Definition df-2o
StepHypRef Expression
1 c2o 7441 . 2 class 2𝑜
2 c1o 7440 . . 3 class 1𝑜
32csuc 5642 . 2 class suc 1𝑜
41, 3wceq 1475 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff setvar class
This definition is referenced by:  2on  7455  2on0  7456  df2o3  7460  ondif2  7469  o1p1e2  7507  o2p2e4  7508  oneo  7548  2onn  7607  nnm2  7616  nnneo  7618  nneob  7619  snnen2o  8034  1sdom2  8044  1sdom  8048  en2  8081  pm54.43  8709  en2eleq  8714  en2other2  8715  infxpenc  8724  infxpenc2  8728  pm110.643ALT  8883  fin1a2lem4  9108  cfpwsdom  9285  canthp1lem2  9354  pwxpndom2  9366  tsk2  9466  hash2  13054  f1otrspeq  17690  pmtrf  17698  pmtrmvd  17699  pmtrfinv  17704  efgmnvl  17950  isnzr2  19084  sltval2  31053  nosgnn0  31055  sltsolem1  31067  bj-2ex  32132  1oequni2o  32392  finxpreclem3  32406  finxpreclem4  32407  finxpsuclem  32410  finxp2o  32412  pw2f1ocnv  36622  pwfi2f1o  36684  clsk1indlem1  37363
  Copyright terms: Public domain W3C validator