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

Definition df-2o 6754
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 6747 . 2  class  2o
2 c1o 6746 . . 3  class  1o
32csuc 4612 . 2  class  suc  1o
41, 3wceq 1653 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6761  2on0  6762  df2o3  6766  ondif2  6775  o1p1e2  6813  oneo  6853  2onn  6912  nnm2  6921  nnneo  6923  nneob  6924  1sdom2  7336  1sdom  7340  en2  7373  pm54.43  7918  infxpenc  7930  infxpenc2  7934  pm110.643ALT  8089  fin1a2lem4  8314  cfpwsdom  8490  canthp1lem2  8559  pwxpndom2  8571  tsk2  8671  hash2  11705  efgmnvl  15377  isnzr2  16365  sltval2  25642  nosgnn0  25644  sltsolem1  25654  pw2f1ocnv  27146  pwfi2f1o  27275  en2eleq  27396  en2other2  27397  f1otrspeq  27405  pmtrf  27412  pmtrmvd  27413  pmtrfinv  27417
  Copyright terms: Public domain W3C validator