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 8089
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 8082 . 2 class 1o
2 c0 4246 . . 3 class
32csuc 6165 . 2 class suc ∅
41, 3wceq 1538 1 wff 1o = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  8096  df1o2  8103  ordgt0ge1  8109  oa1suc  8143  o2p2e4  8153  om1  8155  oe1  8157  oelim2  8208  nnecl  8226  1onn  8252  omabs  8261  nnm1  8262  0sdom1dom  8704  ackbij1lem14  9648  aleph1  9986  cfpwsdom  9999  nlt1pi  10321  indpi  10322  hash1  13765  aleph1re  15594  bnj168  32114  satfv1  32724  fmla1  32748  sltval2  33277  sltsolem1  33294  nosepnelem  33298  nolt02o  33313  rankeq1o  33746  finxp1o  34810  finxpreclem4  34812  finxp00  34820  aleph1min  40253  clsk1indlem1  40745
  Copyright terms: Public domain W3C validator