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

Definition df-1o 6727
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 6720 . 2  class  1o
2 c0 3630 . . 3  class  (/)
32csuc 4586 . 2  class  suc  (/)
41, 3wceq 1653 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6734  df1o2  6739  ordgt0ge1  6744  oa1suc  6778  om1  6788  oe1  6790  oelim2  6841  nnecl  6859  1onn  6885  omabs  6893  nnm1  6894  0sdom1dom  7309  ackbij1lem14  8118  aleph1  8451  cfpwsdom  8464  nlt1pi  8788  indpi  8789  hash1  11678  aleph1re  12849  sltval2  25616  sltsolem1  25628  rankeq1o  26117  bnj168  29171
  Copyright terms: Public domain W3C validator