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

Definition df-1o 6411
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
df-1o  |-  1o  =  suc  (/)

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 6404 . 2  class  1o
2 c0 3422 . . 3  class  (/)
32csuc 4362 . 2  class  suc  (/)
41, 3wceq 1353 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6418  df1o2  6424  ordgt0ge1  6430  oa1suc  6462  1onn  6515  nnm1  6520  nlt1pig  7328  indpi  7329  1tonninf  10423  hash1  10772  012of  14394  2o01f  14395  pwle2  14397  isomninnlem  14427  iswomninnlem  14446  ismkvnnlem  14449
  Copyright terms: Public domain W3C validator