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

Definition df-1o 6716
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 6709 . 2  class  1o
2 c0 3620 . . 3  class  (/)
32csuc 4575 . 2  class  suc  (/)
41, 3wceq 1652 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6723  df1o2  6728  ordgt0ge1  6733  oa1suc  6767  om1  6777  oe1  6779  oelim2  6830  nnecl  6848  1onn  6874  omabs  6882  nnm1  6883  0sdom1dom  7298  ackbij1lem14  8105  aleph1  8438  cfpwsdom  8451  nlt1pi  8775  indpi  8776  hash1  11665  aleph1re  12836  sltval2  25603  sltsolem1  25615  rankeq1o  26104  bnj168  29034
  Copyright terms: Public domain W3C validator