Theorem ditgeq12i

Description: Equality inference for the directed integral. (Contributed by GG, 1-Sep-2025)

	Ref	Expression
Hypotheses	ditgeq12i.1	|- A = B
	ditgeq12i.2	|- C = D
Assertion	ditgeq12i	|- S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x

Proof

Step	Hyp	Ref	Expression
1		ditgeq12i.1	|- A = B
2		ditgeq12i.2	|- C = D
3		eqid	|- E = E
4	1 2 3	ditgeq123i	|- S_ [ A -> C ] E _d x = S_ [ B -> D ] E _d x