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

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

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 6905 . 2
2 c0 3632 . . 3
32csuc 4716 . 2
41, 3wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  1on  6919  df1o2  6924  ordgt0ge1  6929  oa1suc  6963  om1  6973  oe1  6975  oelim2  7026  nnecl  7044  1onn  7070  omabs  7078  nnm1  7079  0sdom1dom  7502  ackbij1lem14  8394  aleph1  8727  cfpwsdom  8740  nlt1pi  9067  indpi  9068  hash1  12154  aleph1re  13519  sltval2  27766  sltsolem1  27778  rankeq1o  28178  bnj168  31650  bj-1ex  32342
  Copyright terms: Public domain W3C validator