| Mathbox for Gino Giotto |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > Mathboxes > cbvditgdavw | Structured version Visualization version GIF version | ||
| Description: Change bound variable in a directed integral. Deduction form. (Contributed by GG, 14-Aug-2025.) |
| Ref | Expression |
|---|---|
| cbvditgdavw.1 | ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) |
| Ref | Expression |
|---|---|
| cbvditgdavw | ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbvditgdavw.1 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 = 𝑦) → 𝐶 = 𝐷) | |
| 2 | 1 | cbvitgdavw 36518 | . . 3 ⊢ (𝜑 → ∫(𝐴(,)𝐵)𝐶 d𝑥 = ∫(𝐴(,)𝐵)𝐷 d𝑦) |
| 3 | 1 | cbvitgdavw 36518 | . . . 4 ⊢ (𝜑 → ∫(𝐵(,)𝐴)𝐶 d𝑥 = ∫(𝐵(,)𝐴)𝐷 d𝑦) |
| 4 | 3 | negeqd 11379 | . . 3 ⊢ (𝜑 → -∫(𝐵(,)𝐴)𝐶 d𝑥 = -∫(𝐵(,)𝐴)𝐷 d𝑦) |
| 5 | 2, 4 | ifeq12d 4477 | . 2 ⊢ (𝜑 → if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥) = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐷 d𝑦, -∫(𝐵(,)𝐴)𝐷 d𝑦)) |
| 6 | df-ditg 25833 | . 2 ⊢ ⨜[𝐴 → 𝐵]𝐶 d𝑥 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐶 d𝑥, -∫(𝐵(,)𝐴)𝐶 d𝑥) | |
| 7 | df-ditg 25833 | . 2 ⊢ ⨜[𝐴 → 𝐵]𝐷 d𝑦 = if(𝐴 ≤ 𝐵, ∫(𝐴(,)𝐵)𝐷 d𝑦, -∫(𝐵(,)𝐴)𝐷 d𝑦) | |
| 8 | 5, 6, 7 | 3eqtr4g 2799 | 1 ⊢ (𝜑 → ⨜[𝐴 → 𝐵]𝐶 d𝑥 = ⨜[𝐴 → 𝐵]𝐷 d𝑦) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 396 = wceq 1547 ifcif 4455 class class class wbr 5073 (class class class)co 7357 ≤ cle 11172 -cneg 11370 (,)cioo 13290 ∫citg 25604 ⨜cdit 25832 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-ext 2711 |
| This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-sb 2074 df-clab 2718 df-cleq 2731 df-clel 2814 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4263 df-if 4456 df-sn 4557 df-pr 4559 df-op 4563 df-uni 4840 df-br 5074 df-opab 5136 df-mpt 5155 df-xp 5625 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6253 df-iota 6442 df-fv 6494 df-ov 7360 df-oprab 7361 df-mpo 7362 df-frecs 8222 df-wrecs 8253 df-recs 8302 df-rdg 8340 df-neg 11372 df-seq 13956 df-sum 15641 df-itg 25609 df-ditg 25833 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |