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

Definition df-7 10961
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 10952 . 2 class 7
2 c6 10951 . . 3 class 6
3 c1 9816 . . 3 class 1
4 caddc 9818 . . 3 class +
52, 3, 4co 6549 . 2 class (6 + 1)
61, 5wceq 1475 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7re  10980  7pos  10997  7m1e6  11018  6p1e7  11033  4p3e7  11040  5p2e7  11042  6p2e8  11046  7nn  11067  6lt7  11086  7p7e14  11485  8p7e15  11493  9p7e16  11501  9p8e17  11502  7t7e49  11529  8t7e56  11537  9t7e63  11544  7prm  15655  17prm  15662  37prm  15666  317prm  15671  log2ublem2  24474  log2ublem3  24475  bclbnd  24805  bposlem8  24816  lgsdir2lem3  24852  2lgslem3d  24924  problem4  30816  rmydioph  36599  expdiophlem2  36607  fmtno5  40007  257prm  40011  2exp7  40052  127prm  40053  7odd  40159  stgoldbwt  40198
  Copyright terms: Public domain W3C validator