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

Definition df-1o 7132
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 7125 . 2  class  1o
2 c0 3770 . . 3  class  (/)
32csuc 4870 . 2  class  suc  (/)
41, 3wceq 1383 1  wff  1o  =  suc  (/)
Colors of variables: wff setvar class
This definition is referenced by:  1on  7139  df1o2  7144  ordgt0ge1  7149  oa1suc  7183  om1  7193  oe1  7195  oelim2  7246  nnecl  7264  1onn  7290  omabs  7298  nnm1  7299  0sdom1dom  7719  ackbij1lem14  8616  aleph1  8949  cfpwsdom  8962  nlt1pi  9287  indpi  9288  hash1  12448  aleph1re  13855  sltval2  29391  sltsolem1  29403  rankeq1o  29803  bnj168  33518  bj-1ex  34255
  Copyright terms: Public domain W3C validator