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

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

Detailed syntax breakdown of Definition df-5
StepHypRef Expression
1 c5 8793 . 2  class  5
2 c4 8792 . . 3  class  4
3 c1 7640 . . 3  class  1
4 caddc 7642 . . 3  class  +
52, 3, 4co 5777 . 2  class  ( 4  +  1 )
61, 5wceq 1331 1  wff  5  =  ( 4  +  1 )
Colors of variables: wff set class
This definition is referenced by:  5re  8818  5pos  8839  5m1e4  8861  4p1e5  8875  3p2e5  8880  4p2e6  8882  5nn  8903  4lt5  8914  5p5e10  9271  6p5e11  9273  7p5e12  9277  8p5e13  9283  8p7e15  9285  9p5e14  9290  9p6e15  9291  5t5e25  9303  6t5e30  9307  7t5e35  9312  8t5e40  9318  9t5e45  9325  fldiv4p1lem1div2  10102  ef01bndlem  11486  ex-exp  13083  ex-fac  13084  ex-bc  13085
  Copyright terms: Public domain W3C validator