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

Definition df-2o 6417
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 6410 . 2  class  2o
2 c1o 6409 . . 3  class  1o
32csuc 4365 . 2  class  suc  1o
41, 3wceq 1353 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6425  2on0  6426  df2o3  6430  o1p1e2  6468  2onn  6521  nnm2  6526  enpr2d  6816  snnen2og  6858  1nen2  6860  pm54.43  7188  en2eleq  7193  en2other2  7194  exmidfodomrlemr  7200  exmidfodomrlemrALT  7201  prarloclemarch2  7417  prarloclemlt  7491  prarloclemn  7497  hash2  10791  bj-el2oss1o  14496  pwle2  14718  nnsf  14724
  Copyright terms: Public domain W3C validator