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

Definition df-2o 5941
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 5934 . 2  2o
2 c1o 5933 . . 3  1o
32csuc 4068 . 2  suc  1o
41, 3wceq 1242 1  2o  suc  1o
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  6476  prarloclemn  6482
  Copyright terms: Public domain W3C validator