| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbviun | Structured version Visualization version GIF version | ||
| Description: Rule used to change the bound variables in an indexed union, with the substitution specified implicitly by the hypothesis. (Contributed by NM, 26-Mar-2006.) (Revised by Andrew Salmon, 25-Jul-2011.) Add disjoint variable condition to avoid ax-13 2377. See cbviung 5038 for a less restrictive version requiring more axioms. (Revised by GG, 20-Jan-2024.) |
| Ref | Expression |
|---|---|
| cbviun.1 | ⊢ Ⅎ𝑦𝐵 |
| cbviun.2 | ⊢ Ⅎ𝑥𝐶 |
| cbviun.3 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
| Ref | Expression |
|---|---|
| cbviun | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbviun.1 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
| 2 | 1 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
| 3 | cbviun.2 | . . . . 5 ⊢ Ⅎ𝑥𝐶 | |
| 4 | 3 | nfcri 2897 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐶 |
| 5 | cbviun.3 | . . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
| 6 | 5 | eleq2d 2827 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
| 7 | 2, 4, 6 | cbvrexw 3307 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶) |
| 8 | 7 | abbii 2809 | . 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} |
| 9 | df-iun 4993 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
| 10 | df-iun 4993 | . 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} | |
| 11 | 8, 9, 10 | 3eqtr4i 2775 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {cab 2714 Ⅎwnfc 2890 ∃wrex 3070 ∪ ciun 4991 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-ex 1780 df-nf 1784 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-iun 4993 |
| This theorem is referenced by: disjxiun 5140 funiunfvf 7269 mpomptsx 8089 dmmpossx 8091 fmpox 8092 ovmptss 8118 iunfi 9383 fsum2dlem 15806 fsumcom2 15810 fsumiun 15857 fprod2dlem 16016 fprodcom2 16020 gsumcom2 19993 fiuncmp 23412 ovolfiniun 25536 ovoliunlem3 25539 ovoliun 25540 finiunmbl 25579 volfiniun 25582 iunmbl 25588 limciun 25929 iunxpssiun1 32581 iuneqfzuzlem 45345 fsumiunss 45590 sge0iunmpt 46433 meaiunincf 46498 meaiuninc3 46500 smfliminf 46846 dmmpossx2 48253 |
| Copyright terms: Public domain | W3C validator |