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

Definition df-1o 7149
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 7142 . 2
2 c0 3784 . . 3
32csuc 4885 . 2
41, 3wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  1on  7156  df1o2  7161  ordgt0ge1  7166  oa1suc  7200  om1  7210  oe1  7212  oelim2  7263  nnecl  7281  1onn  7307  omabs  7315  nnm1  7316  0sdom1dom  7737  ackbij1lem14  8634  aleph1  8967  cfpwsdom  8980  nlt1pi  9305  indpi  9306  hash1  12469  aleph1re  13978  sltval2  29416  sltsolem1  29428  rankeq1o  29828  bnj168  33785  bj-1ex  34507
  Copyright terms: Public domain W3C validator