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

Definition df-2o 6684
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 6677 . 2  class  2o
2 c1o 6676 . . 3  class  1o
32csuc 4543 . 2  class  suc  1o
41, 3wceq 1649 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6691  2on0  6692  df2o3  6696  ondif2  6705  o1p1e2  6743  oneo  6783  2onn  6842  nnm2  6851  nnneo  6853  nneob  6854  1sdom2  7266  1sdom  7270  en2  7303  pm54.43  7843  infxpenc  7855  infxpenc2  7859  pm110.643ALT  8014  fin1a2lem4  8239  cfpwsdom  8415  canthp1lem2  8484  pwxpndom2  8496  tsk2  8596  hash2  11629  efgmnvl  15301  isnzr2  16289  sltval2  25524  nosgnn0  25526  sltsolem1  25536  pw2f1ocnv  26998  pwfi2f1o  27128  en2eleq  27249  en2other2  27250  f1otrspeq  27258  pmtrf  27265  pmtrmvd  27266  pmtrfinv  27270
  Copyright terms: Public domain W3C validator