Theorem ditgeq3i

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

	Ref	Expression
Hypothesis	ditgeq3i.1	⊢ 𝐶 = 𝐷
Assertion	ditgeq3i	⊢ ⨜ [ 𝐴 → 𝐵 ] 𝐶 d 𝑥 = ⨜ [ 𝐴 → 𝐵 ] 𝐷 d 𝑥

Proof

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