Metamath Proof Explorer


Theorem ditgeq3dv

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

Ref Expression
Hypothesis ditgeq3dv.1 φxD=E
Assertion ditgeq3dv φABDdx=ABEdx

Proof

Step Hyp Ref Expression
1 ditgeq3dv.1 φxD=E
2 1 ralrimiva φxD=E
3 ditgeq3 xD=EABDdx=ABEdx
4 2 3 syl φABDdx=ABEdx