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 7793
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 7786 . 2 class 2𝑜
2 c1o 7785 . . 3 class 1𝑜
32csuc 5938 . 2 class suc 1𝑜
41, 3wceq 1637 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff setvar class
This definition is referenced by:  2on  7801  2on0  7802  df2o3  7806  ondif2  7815  o1p1e2  7853  o2p2e4  7854  oneo  7894  2onn  7953  nnm2  7962  nnneo  7964  nneob  7965  snnen2o  8384  1sdom2  8394  1sdom  8398  en2  8431  pm54.43  9105  en2eleq  9110  en2other2  9111  infxpenc  9120  infxpenc2  9124  pm110.643ALT  9281  fin1a2lem4  9506  cfpwsdom  9687  canthp1lem2  9756  pwxpndom2  9768  tsk2  9868  hash2  13406  f1otrspeq  18064  pmtrf  18072  pmtrmvd  18073  pmtrfinv  18078  efgmnvl  18324  isnzr2  19468  sltval2  32125  nosgnn0  32127  sltsolem1  32142  nosepnelem  32146  nolt02o  32161  bj-2ex  33244  1oequni2o  33527  finxpreclem3  33541  finxpreclem4  33542  finxpsuclem  33545  finxp2o  33547  pw2f1ocnv  38099  pwfi2f1o  38161  clsk1indlem1  38837
  Copyright terms: Public domain W3C validator