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

Definition df-9 9806
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 9797 . 2  class  9
2 c8 9796 . . 3  class  8
3 c1 8733 . . 3  class  1
4 caddc 8735 . . 3  class  +
52, 3, 4co 5819 . 2  class  ( 8  +  1 )
61, 5wceq 1624 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  9820  9pos  9832  8p1e9  9848  5p4e9  9857  6p3e9  9860  7p2e9  9862  8p2e10  9864  9nn  9879  8lt9  9909  9p9e18  10188  9t9e81  10221  19prm  13113  139prm  13119  log2tlbnd  20235  bposlem8  20524  lgsdir2lem5  20560  rmydioph  26506
  Copyright terms: Public domain W3C validator