Description: Equality theorem for an integral. (Contributed by Mario Carneiro, 7Jul2014)
Ref  Expression  

Hypothesis  itgeq2dv.1   ( ( ph /\ x e. A ) > B = C ) 

Assertion  itgeq2dv   ( ph > S. A B _d x = S. A C _d x ) 
Step  Hyp  Ref  Expression 

1  itgeq2dv.1   ( ( ph /\ x e. A ) > B = C ) 

2  1  ralrimiva   ( ph > A. x e. A B = C ) 
3  itgeq2   ( A. x e. A B = C > S. A B _d x = S. A C _d x ) 

4  2 3  syl   ( ph > S. A B _d x = S. A C _d x ) 