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

Definition df-1o 6433
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 6426 . 2  class  1o
2 c0 3416 . . 3  class  (/)
32csuc 4352 . 2  class  suc  (/)
41, 3wceq 1619 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6440  df1o2  6445  ordgt0ge1  6450  oa1suc  6484  om1  6494  oe1  6496  oelim2  6547  nnecl  6565  1onn  6591  omabs  6599  nnm1  6600  0sdom1dom  7014  ackbij1lem14  7813  aleph1  8147  cfpwsdom  8160  nlt1pi  8484  indpi  8485  hash1  11321  aleph1re  12471  sltval2  23664  axsltsolem1  23676  rankeq1o  24162  bnj168  27791
  Copyright terms: Public domain W3C validator