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

Definition df-2o 6032
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 6025 . 2  class  2o
2 c1o 6024 . . 3  class  1o
32csuc 4129 . 2  class  suc  1o
41, 3wceq 1259 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6039  2on0  6040  df2o3  6044  o1p1e2  6078  2onn  6124  nnm2  6128  snnen2og  6352  prarloclemarch2  6574  prarloclemlt  6648  prarloclemn  6654
  Copyright terms: Public domain W3C validator