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

Definition df-2o 6442
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 6435 . 2  class  2o
2 c1o 6434 . . 3  class  1o
32csuc 4383 . 2  class  suc  1o
41, 3wceq 1364 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6450  2on0  6451  df2o3  6455  o1p1e2  6493  2onn  6546  nnm2  6551  enpr2d  6843  snnen2og  6887  1nen2  6889  pm54.43  7219  en2eleq  7224  en2other2  7225  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  prarloclemarch2  7448  prarloclemlt  7522  prarloclemn  7528  hash2  10824  bj-el2oss1o  14987  pwle2  15210  nnsf  15216
  Copyright terms: Public domain W3C validator