Metamath Proof Explorer
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 |
⊢ ( 𝜑 → Σ* 𝑘 ∈ 𝐴 𝐶 = Σ* 𝑘 ∈ 𝐵 𝐷 ) |