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

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

Detailed syntax breakdown of Definition df-1o
StepHypRef Expression
1 c1o 7440 . 2 class 1𝑜
2 c0 3874 . . 3 class
32csuc 5642 . 2 class suc ∅
41, 3wceq 1475 1 wff 1𝑜 = suc ∅
Colors of variables: wff setvar class
This definition is referenced by:  1on  7454  df1o2  7459  ordgt0ge1  7464  oa1suc  7498  om1  7509  oe1  7511  oelim2  7562  nnecl  7580  1onn  7606  omabs  7614  nnm1  7615  0sdom1dom  8043  ackbij1lem14  8938  aleph1  9272  cfpwsdom  9285  nlt1pi  9607  indpi  9608  hash1  13053  aleph1re  14813  bnj168  30052  sltval2  31053  sltsolem1  31067  rankeq1o  31448  bj-1ex  32131  finxp1o  32405  finxpreclem4  32407  finxp00  32415  clsk1indlem1  37363
  Copyright terms: Public domain W3C validator