Metamath Proof Explorer

Theorem ditgeq3i

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

Ref Expression
Hypothesis ditgeq3i.1 
|- C = D
Assertion ditgeq3i 
|- S_ [ A -> B ] C _d x = S_ [ A -> B ] D _d x

Proof

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