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

Definition df-8 9805
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 9796 . 2  class  8
2 c7 9795 . . 3  class  7
3 c1 8733 . . 3  class  1
4 caddc 8735 . . 3  class  +
52, 3, 4co 5819 . 2  class  ( 7  +  1 )
61, 5wceq 1624 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  9819  8pos  9831  7p1e8  9847  4p4e8  9854  5p3e8  9856  6p2e8  9859  7p2e9  9862  8nn  9878  7lt8  9902  8p8e16  10180  9p8e17  10187  9p9e18  10188  8t8e64  10213  9t8e72  10220  log2ub  20239  lgsdir2lem1  20556  lgsdir2lem3  20558  rmydioph  26506
  Copyright terms: Public domain W3C validator