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

Definition df-2o 6411
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 6404 . 2 class 2o
2 c1o 6403 . . 3 class 1o
32csuc 4361 . 2 class suc 1o
41, 3wceq 1353 1 wff 2o = suc 1o
Colors of variables: wff set class
This definition is referenced by:  2on  6419  2on0  6420  df2o3  6424  o1p1e2  6462  2onn  6515  nnm2  6520  enpr2d  6810  snnen2og  6852  1nen2  6854  pm54.43  7182  en2eleq  7187  en2other2  7188  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  prarloclemarch2  7396  prarloclemlt  7470  prarloclemn  7476  hash2  10763  bj-el2oss1o  14148  pwle2  14370  nnsf  14377
  Copyright terms: Public domain W3C validator