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

Definition df-2o 6087
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 6080 . 2  class  2o
2 c1o 6079 . . 3  class  1o
32csuc 4148 . 2  class  suc  1o
41, 3wceq 1285 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6094  2on0  6095  df2o3  6099  o1p1e2  6133  2onn  6182  nnm2  6186  snnen2og  6416  1nen2  6418  pm54.43  6588  en2eleq  6591  en2other2  6592  prarloclemarch2  6741  prarloclemlt  6815  prarloclemn  6821  hash2  9906
  Copyright terms: Public domain W3C validator