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

Definition df-2o 6317
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 6310 . 2  class  2o
2 c1o 6309 . . 3  class  1o
32csuc 4290 . 2  class  suc  1o
41, 3wceq 1331 1  wff  2o  =  suc  1o
Colors of variables: wff set class
This definition is referenced by:  2on  6325  2on0  6326  df2o3  6330  o1p1e2  6367  2onn  6420  nnm2  6424  enpr2d  6714  snnen2og  6756  1nen2  6758  infnninf  7025  nnnninf  7026  pm54.43  7058  en2eleq  7063  en2other2  7064  exmidfodomrlemr  7070  exmidfodomrlemrALT  7071  prarloclemarch2  7246  prarloclemlt  7320  prarloclemn  7326  hash2  10582  bj-el2oss1o  13125  pwle2  13339  nnsf  13347
  Copyright terms: Public domain W3C validator