![]() |
Mathbox for Thierry Arnoux |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > esumeq1 | Structured version Visualization version GIF version |
Description: Equality theorem for an extended sum. (Contributed by Thierry Arnoux, 18-Feb-2017.) |
Ref | Expression |
---|---|
esumeq1 | ⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | eqidd 2796 | . 2 ⊢ (𝐴 = 𝐵 → 𝐶 = 𝐶) | |
3 | 1, 2 | esumeq12d 30914 | 1 ⊢ (𝐴 = 𝐵 → Σ*𝑘 ∈ 𝐴𝐶 = Σ*𝑘 ∈ 𝐵𝐶) |
Colors of variables: wff setvar class |
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 |
Copyright terms: Public domain | W3C validator |