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

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

Detailed syntax breakdown of Definition df-7
StepHypRef Expression
1 c7 10046 . 2  class  7
2 c6 10045 . . 3  class  6
3 c1 8983 . . 3  class  1
4 caddc 8985 . . 3  class  +
52, 3, 4co 6073 . 2  class  ( 6  +  1 )
61, 5wceq 1652 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  10069  7pos  10081  6p1e7  10099  4p3e7  10106  5p2e7  10108  6p2e8  10112  7nn  10130  6lt7  10149  7p7e14  10429  8p7e15  10434  9p7e16  10441  9p8e17  10442  7t7e49  10461  8t7e56  10467  9t7e63  10474  7prm  13425  17prm  13431  37prm  13435  317prm  13440  log2ublem2  20779  log2ublem3  20780  bclbnd  21056  bposlem8  21067  lgsdir2lem3  21101  rmydioph  27066  expdiophlem2  27074
  Copyright terms: Public domain W3C validator