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

Definition df-7 9809
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 9800 . 2  class  7
2 c6 9799 . . 3  class  6
3 c1 8738 . . 3  class  1
4 caddc 8740 . . 3  class  +
52, 3, 4co 5858 . 2  class  ( 6  +  1 )
61, 5wceq 1623 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  9823  7pos  9835  6p1e7  9851  4p3e7  9858  5p2e7  9860  6p2e8  9864  7nn  9882  6lt7  9901  7p7e14  10179  8p7e15  10184  9p7e16  10191  9p8e17  10192  7t7e49  10211  8t7e56  10217  9t7e63  10224  7prm  13112  17prm  13118  37prm  13122  317prm  13127  log2ublem2  20243  log2ublem3  20244  bclbnd  20519  bposlem8  20530  lgsdir2lem3  20564  rmydioph  27107  expdiophlem2  27115
  Copyright terms: Public domain W3C validator