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

Definition df-1o 6479
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 6472 . 2  class  1o
2 c0 3455 . . 3  class  (/)
32csuc 4394 . 2  class  suc  (/)
41, 3wceq 1623 1  wff  1o  =  suc  (/)
Colors of variables: wff set class
This definition is referenced by:  1on  6486  df1o2  6491  ordgt0ge1  6496  oa1suc  6530  om1  6540  oe1  6542  oelim2  6593  nnecl  6611  1onn  6637  omabs  6645  nnm1  6646  0sdom1dom  7060  ackbij1lem14  7859  aleph1  8193  cfpwsdom  8206  nlt1pi  8530  indpi  8531  hash1  11370  aleph1re  12523  sltval2  24310  sltsolem1  24322  rankeq1o  24801  bnj168  28758
  Copyright terms: Public domain W3C validator