This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ditgeq3dv

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

		Ref	Expression
	Hypothesis	ditgeq3dv.1	$⊢ (φ \land x \in ℝ) \to D = E$
	Assertion	ditgeq3dv	$⊢ φ \to \int_{A}^{B} D d x = \int_{A}^{B} E d x$

Step	Hyp	Ref	Expression
1		ditgeq3dv.1	$⊢ (φ \land x \in ℝ) \to D = E$
2	1	ralrimiva	$⊢ φ \to \forall x \in ℝ D = E$
3		ditgeq3	$⊢ \forall x \in ℝ D = E \to \int_{A}^{B} D d x = \int_{A}^{B} E d x$
4	2 3	syl	$⊢ φ \to \int_{A}^{B} D d x = \int_{A}^{B} E d x$