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

Definition df-1o 7029
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 7022 . 2  class  1o
2 c0 3744 . . 3  class  (/)
32csuc 4828 . 2  class  suc  (/)
41, 3wceq 1370 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7036  df1o2  7041  ordgt0ge1  7046  oa1suc  7080  om1  7090  oe1  7092  oelim2  7143  nnecl  7161  1onn  7187  omabs  7195  nnm1  7196  0sdom1dom  7620  ackbij1lem14  8512  aleph1  8845  cfpwsdom  8858  nlt1pi  9185  indpi  9186  hash1  12279  aleph1re  13644  sltval2  27940  sltsolem1  27952  rankeq1o  28352  bnj168  32038  bj-1ex  32759
  Copyright terms: Public domain W3C validator