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

Definition df-2o 6164
Description: Define the ordinal number 2. (Contributed by NM, 18-Feb-2004.)
Assertion
Ref Expression
df-2o 2𝑜 = suc 1𝑜

Detailed syntax breakdown of Definition df-2o
StepHypRef Expression
1 c2o 6157 . 2 class 2𝑜
2 c1o 6156 . . 3 class 1𝑜
32csuc 4183 . 2 class suc 1𝑜
41, 3wceq 1289 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff set class
This definition is referenced by:  2on  6172  2on0  6173  df2o3  6177  o1p1e2  6211  2onn  6260  nnm2  6264  snnen2og  6555  1nen2  6557  infnninf  6784  nnnninf  6785  pm54.43  6797  en2eleq  6800  en2other2  6801  exmidfodomrlemr  6807  exmidfodomrlemrALT  6808  prarloclemarch2  6957  prarloclemlt  7031  prarloclemn  7037  hash2  10185  nnsf  11552
  Copyright terms: Public domain W3C validator