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

Definition df-1o 6476
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 6469 . 2  class  1o
2 c0 3458 . . 3  class  (/)
32csuc 4395 . 2  class  suc  (/)
41, 3wceq 1625 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6483  df1o2  6488  ordgt0ge1  6493  oa1suc  6527  om1  6537  oe1  6539  oelim2  6590  nnecl  6608  1onn  6634  omabs  6642  nnm1  6643  0sdom1dom  7057  ackbij1lem14  7856  aleph1  8190  cfpwsdom  8203  nlt1pi  8527  indpi  8528  hash1  11366  aleph1re  12519  sltval2  23712  axsltsolem1  23724  rankeq1o  24210  bnj168  28027
  Copyright terms: Public domain W3C validator