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

Definition df-2o 6002
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 5995 . 2 class 2𝑜
2 c1o 5994 . . 3 class 1𝑜
32csuc 4102 . 2 class suc 1𝑜
41, 3wceq 1243 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff set class
This definition is referenced by:  2on  6009  2on0  6010  df2o3  6014  o1p1e2  6048  2onn  6094  nnm2  6098  snnen2og  6322  prarloclemarch2  6515  prarloclemlt  6589  prarloclemn  6595
  Copyright terms: Public domain W3C validator