Theorem esumeq1 30915

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 2796	. 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶)
3	1, 2	esumeq12d 30914	1 ⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶)

Syntax hints:   → wi 4   = wceq 1522  Σ^*cesum 30908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-dif 3866  df-un 3868  df-in 3870  df-ss 3878  df-nul 4216  df-if 4386  df-sn 4477  df-pr 4479  df-op 4483  df-uni 4750  df-br 4967  df-opab 5029  df-mpt 5046  df-iota 6194  df-fv 6238  df-ov 7024  df-esum 30909

This theorem is referenced by:  esumrnmpt  30933  esumpad  30936  esumpad2  30937  esumpr  30947  esumpr2  30948  esumfzf  30950  esumpmono  30960  esumcvg  30967  esumcvg2  30968  esum2dlem  30973  measvun  31090  ddemeas  31117  oms0  31177  omssubadd  31180  carsgsigalem  31195  carsgclctunlem1  31197  carsgclctunlem2  31199  carsgclctun  31201  pmeasmono  31204  pmeasadd  31205