Theorem esumeq1 34369

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

Syntax hints:   → wi 4   = wceq 1567  Σ^*cesum 34362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-12 2219  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-ral 3086  df-rab 3423  df-v 3463  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4491  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-iota 6493  df-fv 6545  df-ov 7414  df-esum 34363

This theorem is referenced by:  esumrnmpt  34387  esumpad  34390  esumpad2  34391  esumpr  34401  esumpr2  34402  esumfzf  34404  esumpmono  34414  esumcvg  34421  esumcvg2  34422  esum2dlem  34427  measvun  34544  ddemeas  34571  oms0  34632  omssubadd  34635  carsgsigalem  34650  carsgclctunlem1  34652  carsgclctunlem2  34654  carsgclctun  34656  pmeasmono  34659  pmeasadd  34660