Theorem ditgeq3dv

Description: Equality theorem for the directed integral. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Hypothesis	ditgeq3dv.1	|- ( ( ph /\ x e. RR ) -> D = E )
Assertion	ditgeq3dv	|- ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )

Proof

Step	Hyp	Ref	Expression
1		ditgeq3dv.1	|- ( ( ph /\ x e. RR ) -> D = E )
2	1	ralrimiva	|- ( ph -> A. x e. RR D = E )
3		ditgeq3	|- ( A. x e. RR D = E -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )
4	2 3	syl	|- ( ph -> S_ [ A -> B ] D _d x = S_ [ A -> B ] E _d x )