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

Definition df-2o 6496
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 6489 . 2  class  2o
2 c1o 6488 . . 3  class  1o
32csuc 4410 . 2  class  suc  1o
41, 3wceq 1632 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6503  2on0  6504  df2o3  6508  ondif2  6517  o1p1e2  6555  oneo  6595  2onn  6654  nnm2  6663  nnneo  6665  nneob  6666  1sdom2  7077  1sdom  7081  en2  7110  pm54.43  7649  infxpenc  7661  infxpenc2  7665  pm110.643ALT  7820  fin1a2lem4  8045  cfpwsdom  8222  canthp1lem2  8291  pwxpndom2  8303  tsk2  8403  hash2  11387  efgmnvl  15039  isnzr2  16031  sltval2  24381  nosgnn0  24383  sltsolem1  24393  pw2f1ocnv  27233  pwfi2f1o  27363  en2eleq  27484  en2other2  27485  f1otrspeq  27493  pmtrf  27500  pmtrmvd  27501  pmtrfinv  27505
  Copyright terms: Public domain W3C validator