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 7424
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 7417 . 2 class 1𝑜
2 c0 3873 . . 3 class
32csuc 5627 . 2 class suc ∅
41, 3wceq 1474 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7431  df1o2  7436  ordgt0ge1  7441  oa1suc  7475  om1  7486  oe1  7488  oelim2  7539  nnecl  7557  1onn  7583  omabs  7591  nnm1  7592  0sdom1dom  8020  ackbij1lem14  8915  aleph1  9249  cfpwsdom  9262  nlt1pi  9584  indpi  9585  hash1  13007  aleph1re  14761  bnj168  29845  sltval2  30846  sltsolem1  30860  rankeq1o  31241  bj-1ex  31914  finxp1o  32188  finxpreclem4  32190  finxp00  32198  clsk1indlem1  37146
  Copyright terms: Public domain W3C validator