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 7605
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 7598 . 2 class 1𝑜
2 c0 3948 . . 3 class
32csuc 5763 . 2 class suc ∅
41, 3wceq 1523 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7612  df1o2  7617  ordgt0ge1  7622  oa1suc  7656  om1  7667  oe1  7669  oelim2  7720  nnecl  7738  1onn  7764  omabs  7772  nnm1  7773  0sdom1dom  8199  ackbij1lem14  9093  aleph1  9431  cfpwsdom  9444  nlt1pi  9766  indpi  9767  hash1  13230  aleph1re  15018  bnj168  30924  sltval2  31934  sltsolem1  31951  nosepnelem  31955  nolt02o  31970  rankeq1o  32403  bj-1ex  33063  finxp1o  33359  finxpreclem4  33361  finxp00  33369  clsk1indlem1  38660
  Copyright terms: Public domain W3C validator