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

Definition df-1o 6683
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 6676 . 2  class  1o
2 c0 3588 . . 3  class  (/)
32csuc 4543 . 2  class  suc  (/)
41, 3wceq 1649 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6690  df1o2  6695  ordgt0ge1  6700  oa1suc  6734  om1  6744  oe1  6746  oelim2  6797  nnecl  6815  1onn  6841  omabs  6849  nnm1  6850  0sdom1dom  7265  ackbij1lem14  8069  aleph1  8402  cfpwsdom  8415  nlt1pi  8739  indpi  8740  hash1  11628  aleph1re  12799  sltval2  25524  sltsolem1  25536  rankeq1o  26016  bnj168  28803
  Copyright terms: Public domain W3C validator