Theorem ditgeq12i

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

	Ref	Expression
Hypotheses	ditgeq12i.1	⊢ 𝐴 = 𝐵
	ditgeq12i.2	⊢ 𝐶 = 𝐷
Assertion	ditgeq12i	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐸 d 𝑥

Proof

Step	Hyp	Ref	Expression
1		ditgeq12i.1	⊢ 𝐴 = 𝐵
2		ditgeq12i.2	⊢ 𝐶 = 𝐷
3		eqid	⊢ 𝐸 = 𝐸
4	1 2 3	ditgeq123i	⊢ ⨜ [ 𝐴 → 𝐶 ] 𝐸 d 𝑥 = ⨜ [ 𝐵 → 𝐷 ] 𝐸 d 𝑥