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

Definition df-2o 6477
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 6470 . 2  class  2o
2 c1o 6469 . . 3  class  1o
32csuc 4395 . 2  class  suc  1o
41, 3wceq 1625 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6484  2on0  6485  df2o3  6489  ondif2  6498  o1p1e2  6536  oneo  6576  2onn  6635  nnm2  6644  nnneo  6646  nneob  6647  1sdom2  7058  1sdom  7062  en2  7091  pm54.43  7630  infxpenc  7642  infxpenc2  7646  pm110.643ALT  7801  fin1a2lem4  8026  cfpwsdom  8203  canthp1lem2  8272  pwxpndom2  8284  tsk2  8384  hash2  11367  efgmnvl  15019  isnzr2  16011  sltval2  23712  nosgnn0  23714  axsltsolem1  23724  pw2f1ocnv  26531  pwfi2f1o  26661  en2eleq  26782  en2other2  26783  f1otrspeq  26791  pmtrf  26798  pmtrmvd  26799  pmtrfinv  26803
  Copyright terms: Public domain W3C validator