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 10931
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 10922 . 2 class 7
2 c6 10921 . . 3 class 6
3 c1 9793 . . 3 class 1
4 caddc 9795 . . 3 class +
52, 3, 4co 6527 . 2 class (6 + 1)
61, 5wceq 1474 1 wff 7 = (6 + 1)
Colors of variables: wff setvar class
This definition is referenced by:  7re  10950  7pos  10967  7m1e6  10988  6p1e7  11003  4p3e7  11010  5p2e7  11012  6p2e8  11016  7nn  11037  6lt7  11056  7p7e14  11441  8p7e15  11449  9p7e16  11457  9p8e17  11458  7t7e49  11485  8t7e56  11493  9t7e63  11500  7prm  15601  17prm  15608  37prm  15612  317prm  15617  log2ublem2  24391  log2ublem3  24392  bclbnd  24722  bposlem8  24733  lgsdir2lem3  24769  2lgslem3d  24841  problem4  30622  rmydioph  36395  expdiophlem2  36403  fmtno5  39805  257prm  39809  2exp7  39850  127prm  39851  7odd  39957  stgoldbwt  39996
  Copyright terms: Public domain W3C validator