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

Definition df-1o 7799
Description: Define the ordinal number 1. (Contributed by NM, 29-Oct-1995.)
Assertion
Ref Expression
df-1o 1𝑜 = suc ∅

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 7792 . 2 class 1𝑜
2 c0 4123 . . 3 class
32csuc 5945 . 2 class suc ∅
41, 3wceq 1637 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7806  df1o2  7812  ordgt0ge1  7817  oa1suc  7851  om1  7862  oe1  7864  oelim2  7915  nnecl  7933  1onn  7959  omabs  7967  nnm1  7968  0sdom1dom  8400  ackbij1lem14  9343  aleph1  9681  cfpwsdom  9694  nlt1pi  10016  indpi  10017  hash1  13412  aleph1re  15197  bnj168  31127  sltval2  32135  sltsolem1  32152  nosepnelem  32156  nolt02o  32171  rankeq1o  32604  finxp1o  33547  finxpreclem4  33549  finxp00  33557  clsk1indlem1  38844
  Copyright terms: Public domain W3C validator