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

Definition df-2o 6396
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 6389 . 2  class  2o
2 c1o 6388 . . 3  class  1o
32csuc 4350 . 2  class  suc  1o
41, 3wceq 1348 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6404  2on0  6405  df2o3  6409  o1p1e2  6447  2onn  6500  nnm2  6505  enpr2d  6795  snnen2og  6837  1nen2  6839  pm54.43  7167  en2eleq  7172  en2other2  7173  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  prarloclemarch2  7381  prarloclemlt  7455  prarloclemn  7461  hash2  10747  bj-el2oss1o  13809  pwle2  14031  nnsf  14038
  Copyright terms: Public domain W3C validator