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

Definition df-2o 6244
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 6237 . 2  class  2o
2 c1o 6236 . . 3  class  1o
32csuc 4225 . 2  class  suc  1o
41, 3wceq 1299 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6252  2on0  6253  df2o3  6257  o1p1e2  6294  2onn  6347  nnm2  6351  snnen2og  6682  1nen2  6684  infnninf  6934  nnnninf  6935  pm54.43  6957  en2eleq  6960  en2other2  6961  exmidfodomrlemr  6967  exmidfodomrlemrALT  6968  prarloclemarch2  7128  prarloclemlt  7202  prarloclemn  7208  hash2  10399  pwle2  12779  nnsf  12783
  Copyright terms: Public domain W3C validator