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

Definition df-2o 6663
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 6656 . 2  class  2o
2 c1o 6655 . . 3  class  1o
32csuc 4526 . 2  class  suc  1o
41, 3wceq 1649 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6670  2on0  6671  df2o3  6675  ondif2  6684  o1p1e2  6722  oneo  6762  2onn  6821  nnm2  6830  nnneo  6832  nneob  6833  1sdom2  7245  1sdom  7249  en2  7282  pm54.43  7822  infxpenc  7834  infxpenc2  7838  pm110.643ALT  7993  fin1a2lem4  8218  cfpwsdom  8394  canthp1lem2  8463  pwxpndom2  8475  tsk2  8575  hash2  11603  efgmnvl  15275  isnzr2  16263  sltval2  25336  nosgnn0  25338  sltsolem1  25348  pw2f1ocnv  26801  pwfi2f1o  26931  en2eleq  27052  en2other2  27053  f1otrspeq  27061  pmtrf  27068  pmtrmvd  27069  pmtrfinv  27073
  Copyright terms: Public domain W3C validator