MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-1o Unicode version

Definition df-1o 6660
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 6653 . 2  class  1o
2 c0 3571 . . 3  class  (/)
32csuc 4524 . 2  class  suc  (/)
41, 3wceq 1649 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6667  df1o2  6672  ordgt0ge1  6677  oa1suc  6711  om1  6721  oe1  6723  oelim2  6774  nnecl  6792  1onn  6818  omabs  6826  nnm1  6827  0sdom1dom  7242  ackbij1lem14  8046  aleph1  8379  cfpwsdom  8392  nlt1pi  8716  indpi  8717  hash1  11600  aleph1re  12771  sltval2  25334  sltsolem1  25346  rankeq1o  25826  bnj168  28435
  Copyright terms: Public domain W3C validator