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 7727
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 7720 . 2 class 1𝑜
2 c0 4056 . . 3 class
32csuc 5884 . 2 class suc ∅
41, 3wceq 1630 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7734  df1o2  7739  ordgt0ge1  7744  oa1suc  7778  om1  7789  oe1  7791  oelim2  7842  nnecl  7860  1onn  7886  omabs  7894  nnm1  7895  0sdom1dom  8321  ackbij1lem14  9245  aleph1  9583  cfpwsdom  9596  nlt1pi  9918  indpi  9919  hash1  13382  aleph1re  15171  bnj168  31103  sltval2  32113  sltsolem1  32130  nosepnelem  32134  nolt02o  32149  rankeq1o  32582  bj-1ex  33242  finxp1o  33538  finxpreclem4  33540  finxp00  33548  clsk1indlem1  38843
  Copyright terms: Public domain W3C validator