Metamath Proof Explorer


Theorem esumeq12dva

Description: Equality deduction for extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017) (Revised by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumeq12dva.1 ( 𝜑𝐴 = 𝐵 )
esumeq12dva.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 = 𝐷 )
Assertion esumeq12dva ( 𝜑 → Σ* 𝑘𝐴 𝐶 = Σ* 𝑘𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 esumeq12dva.1 ( 𝜑𝐴 = 𝐵 )
2 esumeq12dva.2 ( ( 𝜑𝑘𝐴 ) → 𝐶 = 𝐷 )
3 nfv 𝑘 𝜑
4 3 1 2 esumeq12dvaf ( 𝜑 → Σ* 𝑘𝐴 𝐶 = Σ* 𝑘𝐵 𝐷 )