ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-2o Unicode version

Definition df-2o 6136
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 6129 . 2  class  2o
2 c1o 6128 . . 3  class  1o
32csuc 4166 . 2  class  suc  1o
41, 3wceq 1287 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6144  2on0  6145  df2o3  6149  o1p1e2  6183  2onn  6232  nnm2  6236  snnen2og  6527  1nen2  6529  infnninf  6749  nnnninf  6750  pm54.43  6762  en2eleq  6765  en2other2  6766  exmidfodomrlemr  6772  exmidfodomrlemrALT  6773  prarloclemarch2  6922  prarloclemlt  6996  prarloclemn  7002  hash2  10116  nnsf  11333
  Copyright terms: Public domain W3C validator