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

Definition df-7 9825
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 9816 . 2  class  7
2 c6 9815 . . 3  class  6
3 c1 8754 . . 3  class  1
4 caddc 8756 . . 3  class  +
52, 3, 4co 5874 . 2  class  ( 6  +  1 )
61, 5wceq 1632 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  9839  7pos  9851  6p1e7  9867  4p3e7  9874  5p2e7  9876  6p2e8  9880  7nn  9898  6lt7  9917  7p7e14  10195  8p7e15  10200  9p7e16  10207  9p8e17  10208  7t7e49  10227  8t7e56  10233  9t7e63  10240  7prm  13128  17prm  13134  37prm  13138  317prm  13143  log2ublem2  20259  log2ublem3  20260  bclbnd  20535  bposlem8  20546  lgsdir2lem3  20580  rmydioph  27210  expdiophlem2  27218
  Copyright terms: Public domain W3C validator