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

Definition df-2o 5941
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 5934 . 2 class 2𝑜
2 c1o 5933 . . 3 class 1𝑜
32csuc 4068 . 2 class suc 1𝑜
41, 3wceq 1242 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff set class
This definition is referenced by:  2on  5948  2on0  5949  df2o3  5953  o1p1e2  5987  2onn  6030  nnm2  6034  prarloclemarch2  6402  prarloclemlt  6475  prarloclemn  6481
  Copyright terms: Public domain W3C validator