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

Definition df-8 9855
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 9846 . 2  class  8
2 c7 9845 . . 3  class  7
3 c1 8783 . . 3  class  1
4 caddc 8785 . . 3  class  +
52, 3, 4co 5900 . 2  class  ( 7  +  1 )
61, 5wceq 1633 1  wff  8  =  ( 7  +  1 )
Colors of variables: wff set class
This definition is referenced by:  8re  9869  8pos  9881  7p1e8  9899  4p4e8  9906  5p3e8  9908  6p2e8  9911  7p2e9  9914  8nn  9930  7lt8  9954  8p8e16  10232  9p8e17  10239  9p9e18  10240  8t8e64  10265  9t8e72  10272  log2ub  20298  lgsdir2lem1  20615  lgsdir2lem3  20617  rmydioph  26255
  Copyright terms: Public domain W3C validator