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

Definition df-1o 6365
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 6358 . 2  class  1o
2 c0 3395 . . 3  class  (/)
32csuc 4327 . 2  class  suc  (/)
41, 3wceq 1335 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6372  df1o2  6378  ordgt0ge1  6384  oa1suc  6416  1onn  6469  nnm1  6473  nlt1pig  7263  indpi  7264  1tonninf  10348  hash1  10696  012of  13638  2o01f  13639  pwle2  13641  isomninnlem  13672  iswomninnlem  13691  ismkvnnlem  13694
  Copyright terms: Public domain W3C validator