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

Definition df-8 10065
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 10056 . 2  class  8
2 c7 10055 . . 3  class  7
3 c1 8992 . . 3  class  1
4 caddc 8994 . . 3  class  +
52, 3, 4co 6082 . 2  class  ( 7  +  1 )
61, 5wceq 1653 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  10079  8pos  10091  7p1e8  10109  4p4e8  10116  5p3e8  10118  6p2e8  10121  7p2e9  10124  8nn  10140  7lt8  10164  8p8e16  10444  9p8e17  10451  9p9e18  10452  8t8e64  10477  9t8e72  10484  log2ub  20790  lgsdir2lem1  21108  lgsdir2lem3  21110  rmydioph  27086
  Copyright terms: Public domain W3C validator