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

Definition df-1o 6653
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 6646 . 2  class  1o
2 c0 3564 . . 3  class  (/)
32csuc 4517 . 2  class  suc  (/)
41, 3wceq 1649 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6660  df1o2  6665  ordgt0ge1  6670  oa1suc  6704  om1  6714  oe1  6716  oelim2  6767  nnecl  6785  1onn  6811  omabs  6819  nnm1  6820  0sdom1dom  7235  ackbij1lem14  8039  aleph1  8372  cfpwsdom  8385  nlt1pi  8709  indpi  8710  hash1  11593  aleph1re  12764  sltval2  25327  sltsolem1  25339  rankeq1o  25819  bnj168  28428
  Copyright terms: Public domain W3C validator