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

Definition df-1o 6442
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 6435 . 2  class  1o
2 c0 3437 . . 3  class  (/)
32csuc 4383 . 2  class  suc  (/)
41, 3wceq 1364 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6449  df1o2  6455  ordgt0ge1  6461  oa1suc  6493  1onn  6546  nnm1  6551  nlt1pig  7371  indpi  7372  1tonninf  10473  hash1  10826  012of  15224  2o01f  15225  pwle2  15227  isomninnlem  15257  iswomninnlem  15276  ismkvnnlem  15279
  Copyright terms: Public domain W3C validator