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

Definition df-2o 6033
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 6026 . 2 class 2𝑜
2 c1o 6025 . . 3 class 1𝑜
32csuc 4130 . 2 class suc 1𝑜
41, 3wceq 1259 1 wff 2𝑜 = suc 1𝑜
Colors of variables: wff set class
This definition is referenced by:  2on  6040  2on0  6041  df2o3  6045  o1p1e2  6079  2onn  6125  nnm2  6129  snnen2og  6353  prarloclemarch2  6575  prarloclemlt  6649  prarloclemn  6655
  Copyright terms: Public domain W3C validator