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

Definition df-7 10068
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 10059 . 2  class  7
2 c6 10058 . . 3  class  6
3 c1 8996 . . 3  class  1
4 caddc 8998 . . 3  class  +
52, 3, 4co 6084 . 2  class  ( 6  +  1 )
61, 5wceq 1653 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  10082  7pos  10094  6p1e7  10112  4p3e7  10119  5p2e7  10121  6p2e8  10125  7nn  10143  6lt7  10162  7p7e14  10442  8p7e15  10447  9p7e16  10454  9p8e17  10455  7t7e49  10474  8t7e56  10480  9t7e63  10487  7prm  13438  17prm  13444  37prm  13448  317prm  13453  log2ublem2  20792  log2ublem3  20793  bclbnd  21069  bposlem8  21080  lgsdir2lem3  21114  rmydioph  27099  expdiophlem2  27107
  Copyright terms: Public domain W3C validator