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

Definition df-7 10019
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 10010 . 2  class  7
2 c6 10009 . . 3  class  6
3 c1 8947 . . 3  class  1
4 caddc 8949 . . 3  class  +
52, 3, 4co 6040 . 2  class  ( 6  +  1 )
61, 5wceq 1649 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  10033  7pos  10045  6p1e7  10063  4p3e7  10070  5p2e7  10072  6p2e8  10076  7nn  10094  6lt7  10113  7p7e14  10393  8p7e15  10398  9p7e16  10405  9p8e17  10406  7t7e49  10425  8t7e56  10431  9t7e63  10438  7prm  13388  17prm  13394  37prm  13398  317prm  13403  log2ublem2  20740  log2ublem3  20741  bclbnd  21017  bposlem8  21028  lgsdir2lem3  21062  rmydioph  26975  expdiophlem2  26983
  Copyright terms: Public domain W3C validator