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

Definition df-2o 6480
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 6473 . 2  class  2o
2 c1o 6472 . . 3  class  1o
32csuc 4394 . 2  class  suc  1o
41, 3wceq 1623 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6487  2on0  6488  df2o3  6492  ondif2  6501  o1p1e2  6539  oneo  6579  2onn  6638  nnm2  6647  nnneo  6649  nneob  6650  1sdom2  7061  1sdom  7065  en2  7094  pm54.43  7633  infxpenc  7645  infxpenc2  7649  pm110.643ALT  7804  fin1a2lem4  8029  cfpwsdom  8206  canthp1lem2  8275  pwxpndom2  8287  tsk2  8387  hash2  11371  efgmnvl  15023  isnzr2  16015  sltval2  24310  nosgnn0  24312  sltsolem1  24322  pw2f1ocnv  27130  pwfi2f1o  27260  en2eleq  27381  en2other2  27382  f1otrspeq  27390  pmtrf  27397  pmtrmvd  27398  pmtrfinv  27402
  Copyright terms: Public domain W3C validator