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

Definition df-7 11700
 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 11692 . 2 class 7
2 c6 11691 . . 3 class 6
3 c1 10534 . . 3 class 1
4 caddc 10536 . . 3 class +
52, 3, 4co 7140 . 2 class (6 + 1)
61, 5wceq 1538 1 wff 7 = (6 + 1)
 Colors of variables: wff setvar class This definition is referenced by:  7nn  11724  7re  11725  7cn  11726  7pos  11743  7m1e6  11764  6p1e7  11780  4p3e7  11786  5p2e7  11788  6p2e8  11791  6lt7  11818  7p7e14  12172  8p7e15  12178  9p7e16  12185  9p8e17  12186  7t7e49  12207  8t7e56  12213  9t7e63  12220  2exp7  16421  7prm  16443  17prm  16449  37prm  16453  317prm  16458  log2ublem2  25547  log2ublem3  25548  bclbnd  25878  bposlem8  25889  lgsdir2lem3  25925  problem4  33060  3cubeslem3r  39692  rmydioph  40019  expdiophlem2  40027  fmtno5  44135  257prm  44139  127prm  44177  7odd  44291  stgoldbwt  44355
 Copyright terms: Public domain W3C validator