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

Definition df-2o 6692
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 6685 . 2  class  2o
2 c1o 6684 . . 3  class  1o
32csuc 4551 . 2  class  suc  1o
41, 3wceq 1649 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6699  2on0  6700  df2o3  6704  ondif2  6713  o1p1e2  6751  oneo  6791  2onn  6850  nnm2  6859  nnneo  6861  nneob  6862  1sdom2  7274  1sdom  7278  en2  7311  pm54.43  7851  infxpenc  7863  infxpenc2  7867  pm110.643ALT  8022  fin1a2lem4  8247  cfpwsdom  8423  canthp1lem2  8492  pwxpndom2  8504  tsk2  8604  hash2  11637  efgmnvl  15309  isnzr2  16297  sltval2  25532  nosgnn0  25534  sltsolem1  25544  pw2f1ocnv  27006  pwfi2f1o  27136  en2eleq  27257  en2other2  27258  f1otrspeq  27266  pmtrf  27273  pmtrmvd  27274  pmtrfinv  27278
  Copyright terms: Public domain W3C validator