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

Definition df-1o 6395
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 6388 . 2  class  1o
2 c0 3414 . . 3  class  (/)
32csuc 4350 . 2  class  suc  (/)
41, 3wceq 1348 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6402  df1o2  6408  ordgt0ge1  6414  oa1suc  6446  1onn  6499  nnm1  6504  nlt1pig  7303  indpi  7304  1tonninf  10396  hash1  10746  012of  14028  2o01f  14029  pwle2  14031  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084
  Copyright terms: Public domain W3C validator