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

Definition df-2o 6434
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 6427 . 2  class  2o
2 c1o 6426 . . 3  class  1o
32csuc 4352 . 2  class  suc  1o
41, 3wceq 1619 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6441  2on0  6442  df2o3  6446  ondif2  6455  o1p1e2  6493  oneo  6533  2onn  6592  nnm2  6601  nnneo  6603  nneob  6604  1sdom2  7015  1sdom  7019  en2  7048  pm54.43  7587  infxpenc  7599  infxpenc2  7603  pm110.643ALT  7758  fin1a2lem4  7983  cfpwsdom  8160  canthp1lem2  8229  pwxpndom2  8241  tsk2  8341  hash2  11322  efgmnvl  14971  isnzr2  15963  sltval2  23664  nosgnn0  23666  axsltsolem1  23676  pw2f1ocnv  26483  pwfi2f1o  26613  en2eleq  26734  en2other2  26735  f1otrspeq  26743  pmtrf  26750  pmtrmvd  26751  pmtrfinv  26755
  Copyright terms: Public domain W3C validator