ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-9 Unicode version

Definition df-9 8172
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 8163 . 2  class  9
2 c8 8162 . . 3  class  8
3 c1 7044 . . 3  class  1
4 caddc 7046 . . 3  class  +
52, 3, 4co 5543 . 2  class  ( 8  +  1 )
61, 5wceq 1285 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  8193  9pos  8210  8p1e9  8239  5p4e9  8247  6p3e9  8249  7p2e9  8250  9nn  8267  8lt9  8296  8p2e10  8637  9p9e18  8651  9t9e81  8686
  Copyright terms: Public domain W3C validator