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

Definition df-7 9805
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 9796 . 2  class  7
2 c6 9795 . . 3  class  6
3 c1 8734 . . 3  class  1
4 caddc 8736 . . 3  class  +
52, 3, 4co 5820 . 2  class  ( 6  +  1 )
61, 5wceq 1624 1  wff  7  =  ( 6  +  1 )
Colors of variables: wff set class
This definition is referenced by:  7re  9819  7pos  9831  6p1e7  9847  4p3e7  9854  5p2e7  9856  6p2e8  9860  7nn  9878  6lt7  9897  7p7e14  10175  8p7e15  10180  9p7e16  10187  9p8e17  10188  7t7e49  10207  8t7e56  10213  9t7e63  10220  7prm  13107  17prm  13113  37prm  13117  317prm  13122  log2ublem2  20238  log2ublem3  20239  bclbnd  20514  bposlem8  20525  lgsdir2lem3  20559  rmydioph  26507  expdiophlem2  26515
  Copyright terms: Public domain W3C validator