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

Definition df-9 10067
Description: Define the number 9. (Contributed by NM, 27-May-1999.)
Assertion
Ref Expression
df-9  |-  9  =  ( 8  +  1 )

Detailed syntax breakdown of Definition df-9
StepHypRef Expression
1 c9 10058 . 2  class  9
2 c8 10057 . . 3  class  8
3 c1 8993 . . 3  class  1
4 caddc 8995 . . 3  class  +
52, 3, 4co 6083 . 2  class  ( 8  +  1 )
61, 5wceq 1653 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  10081  9pos  10093  8p1e9  10111  5p4e9  10120  6p3e9  10123  7p2e9  10125  8p2e10  10127  9nn  10142  8lt9  10172  9p9e18  10453  9t9e81  10486  19prm  13442  139prm  13448  log2tlbnd  20787  bposlem8  21077  lgsdir2lem5  21113  rmydioph  27087
  Copyright terms: Public domain W3C validator