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

Definition df-1o 7130
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 7123 . 2  class  1o
2 c0 3785 . . 3  class  (/)
32csuc 4880 . 2  class  suc  (/)
41, 3wceq 1379 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7137  df1o2  7142  ordgt0ge1  7147  oa1suc  7181  om1  7191  oe1  7193  oelim2  7244  nnecl  7262  1onn  7288  omabs  7296  nnm1  7297  0sdom1dom  7717  ackbij1lem14  8613  aleph1  8946  cfpwsdom  8959  nlt1pi  9284  indpi  9285  hash1  12435  aleph1re  13839  sltval2  29021  sltsolem1  29033  rankeq1o  29433  bnj168  32883  bj-1ex  33606
  Copyright terms: Public domain W3C validator