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

Definition df-9 8961
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 8953 . 2  class  9
2 c8 8952 . . 3  class  8
3 c1 7790 . . 3  class  1
4 caddc 7792 . . 3  class  +
52, 3, 4co 5868 . 2  class  ( 8  +  1 )
61, 5wceq 1353 1  wff  9  =  ( 8  +  1 )
Colors of variables: wff set class
This definition is referenced by:  9re  8982  9pos  8999  9m1e8  9021  8p1e9  9035  5p4e9  9043  6p3e9  9045  7p2e9  9046  9nn  9063  8lt9  9092  8p2e10  9439  9p9e18  9453  9t9e81  9488  lgsdir2lem5  14066
  Copyright terms: Public domain W3C validator