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

Definition df-9 9901
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 9892 . 2  class  9
2 c8 9891 . . 3  class  8
3 c1 8828 . . 3  class  1
4 caddc 8830 . . 3  class  +
52, 3, 4co 5945 . 2  class  ( 8  +  1 )
61, 5wceq 1642 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  9915  9pos  9927  8p1e9  9945  5p4e9  9954  6p3e9  9957  7p2e9  9959  8p2e10  9961  9nn  9976  8lt9  10006  9p9e18  10285  9t9e81  10318  19prm  13216  139prm  13222  log2tlbnd  20352  bposlem8  20642  lgsdir2lem5  20678  rmydioph  26430
  Copyright terms: Public domain W3C validator