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

Definition df-1o 6760
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 6753 . 2  class  1o
2 c0 3616 . . 3  class  (/)
32csuc 4618 . 2  class  suc  (/)
41, 3wceq 1654 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6767  df1o2  6772  ordgt0ge1  6777  oa1suc  6811  om1  6821  oe1  6823  oelim2  6874  nnecl  6892  1onn  6918  omabs  6926  nnm1  6927  0sdom1dom  7342  ackbij1lem14  8151  aleph1  8484  cfpwsdom  8497  nlt1pi  8821  indpi  8822  hash1  11711  aleph1re  12882  sltval2  25646  sltsolem1  25658  rankeq1o  26147  bnj168  29271
  Copyright terms: Public domain W3C validator