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

Definition df-2o 6418
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 6411 . 2  class  2o
2 c1o 6410 . . 3  class  1o
32csuc 4366 . 2  class  suc  1o
41, 3wceq 1353 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6426  2on0  6427  df2o3  6431  o1p1e2  6469  2onn  6522  nnm2  6527  enpr2d  6817  snnen2og  6859  1nen2  6861  pm54.43  7189  en2eleq  7194  en2other2  7195  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  prarloclemarch2  7418  prarloclemlt  7492  prarloclemn  7498  hash2  10792  bj-el2oss1o  14529  pwle2  14751  nnsf  14757
  Copyright terms: Public domain W3C validator