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

Definition df-1o 6687
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 6680 . 2  class  1o
2 c0 3592 . . 3  class  (/)
32csuc 4547 . 2  class  suc  (/)
41, 3wceq 1649 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6694  df1o2  6699  ordgt0ge1  6704  oa1suc  6738  om1  6748  oe1  6750  oelim2  6801  nnecl  6819  1onn  6845  omabs  6853  nnm1  6854  0sdom1dom  7269  ackbij1lem14  8073  aleph1  8406  cfpwsdom  8419  nlt1pi  8743  indpi  8744  hash1  11632  aleph1re  12803  sltval2  25528  sltsolem1  25540  rankeq1o  26020  bnj168  28807
  Copyright terms: Public domain W3C validator