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

Definition df-8 10020
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 10011 . 2  class  8
2 c7 10010 . . 3  class  7
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 7  +  1 )
61, 5wceq 1649 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  10034  8pos  10046  7p1e8  10064  4p4e8  10071  5p3e8  10073  6p2e8  10076  7p2e9  10079  8nn  10095  7lt8  10119  8p8e16  10399  9p8e17  10406  9p9e18  10407  8t8e64  10432  9t8e72  10439  log2ub  20742  lgsdir2lem1  21060  lgsdir2lem3  21062  rmydioph  26975
  Copyright terms: Public domain W3C validator