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

Definition df-2o 6717
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 6710 . 2  class  2o
2 c1o 6709 . . 3  class  1o
32csuc 4575 . 2  class  suc  1o
41, 3wceq 1652 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6724  2on0  6725  df2o3  6729  ondif2  6738  o1p1e2  6776  oneo  6816  2onn  6875  nnm2  6884  nnneo  6886  nneob  6887  1sdom2  7299  1sdom  7303  en2  7336  pm54.43  7879  infxpenc  7891  infxpenc2  7895  pm110.643ALT  8050  fin1a2lem4  8275  cfpwsdom  8451  canthp1lem2  8520  pwxpndom2  8532  tsk2  8632  hash2  11666  efgmnvl  15338  isnzr2  16326  sltval2  25603  nosgnn0  25605  sltsolem1  25615  pw2f1ocnv  27099  pwfi2f1o  27228  en2eleq  27349  en2other2  27350  f1otrspeq  27358  pmtrf  27365  pmtrmvd  27366  pmtrfinv  27370
  Copyright terms: Public domain W3C validator