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

Definition df-2o 6662
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 6655 . 2  class  2o
2 c1o 6654 . . 3  class  1o
32csuc 4525 . 2  class  suc  1o
41, 3wceq 1649 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6669  2on0  6670  df2o3  6674  ondif2  6683  o1p1e2  6721  oneo  6761  2onn  6820  nnm2  6829  nnneo  6831  nneob  6832  1sdom2  7244  1sdom  7248  en2  7281  pm54.43  7821  infxpenc  7833  infxpenc2  7837  pm110.643ALT  7992  fin1a2lem4  8217  cfpwsdom  8393  canthp1lem2  8462  pwxpndom2  8474  tsk2  8574  hash2  11602  efgmnvl  15274  isnzr2  16262  sltval2  25335  nosgnn0  25337  sltsolem1  25347  pw2f1ocnv  26800  pwfi2f1o  26930  en2eleq  27051  en2other2  27052  f1otrspeq  27060  pmtrf  27067  pmtrmvd  27068  pmtrfinv  27072
  Copyright terms: Public domain W3C validator