Theorem esumeq1 34275

Description: Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.)

Assertion

Ref	Expression
esumeq1	⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)

Distinct variable groups:   𝐴,𝑘   𝐵,𝑘

Allowed substitution hint:   𝐶(𝑘)

Proof of Theorem esumeq1

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵)
2		eqidd 2753	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	esumeq12d 34274	1 ⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)

Syntax hints:   → wi 4   = wceq 1550  Σ^*cesum 34268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-12 2202  ax-ext 2724

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-ral 3067  df-rab 3405  df-v 3446  df-dif 3898  df-un 3900  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-iota 6462  df-fv 6514  df-ov 7384  df-esum 34269

This theorem is referenced by:  esumrnmpt  34293  esumpad  34296  esumpad2  34297  esumpr  34307  esumpr2  34308  esumfzf  34310  esumpmono  34320  esumcvg  34327  esumcvg2  34328  esum2dlem  34333  measvun  34450  ddemeas  34477  oms0  34538  omssubadd  34541  carsgsigalem  34556  carsgclctunlem1  34558  carsgclctunlem2  34560  carsgclctun  34562  pmeasmono  34565  pmeasadd  34566