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

Definition df-8 9810
Description: Define the number 8. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-8  |-  8  =  ( 7  +  1 )

Detailed syntax breakdown of Definition df-8
StepHypRef Expression
1 c8 9801 . 2  class  8
2 c7 9800 . . 3  class  7
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 7  +  1 )
61, 5wceq 1623 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  9824  8pos  9836  7p1e8  9852  4p4e8  9859  5p3e8  9861  6p2e8  9864  7p2e9  9867  8nn  9883  7lt8  9907  8p8e16  10185  9p8e17  10192  9p9e18  10193  8t8e64  10218  9t8e72  10225  log2ub  20245  lgsdir2lem1  20562  lgsdir2lem3  20564  rmydioph  27107
  Copyright terms: Public domain W3C validator