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 2371. See cbviung 4933 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 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 2884 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
3 | cbviun.2 | . . . . 5 ⊢ Ⅎ𝑥𝐶 | |
4 | 3 | nfcri 2884 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐶 |
5 | cbviun.3 | . . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
6 | 5 | eleq2d 2816 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
7 | 2, 4, 6 | cbvrexw 3340 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶) |
8 | 7 | abbii 2801 | . 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} |
9 | df-iun 4892 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
10 | df-iun 4892 | . 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} | |
11 | 8, 9, 10 | 3eqtr4i 2769 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2112 {cab 2714 Ⅎwnfc 2877 ∃wrex 3052 ∪ ciun 4890 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-11 2160 ax-12 2177 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-ex 1788 df-nf 1792 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-nfc 2879 df-ral 3056 df-rex 3057 df-iun 4892 |
This theorem is referenced by: cbviunv 4935 disjxiun 5036 funiunfvf 7040 mpomptsx 7812 dmmpossx 7814 fmpox 7815 ovmptss 7839 iunfi 8942 fsum2dlem 15297 fsumcom2 15301 fsumiun 15348 fprod2dlem 15505 fprodcom2 15509 gsumcom2 19314 fiuncmp 22255 ovolfiniun 24352 ovoliunlem3 24355 ovoliun 24356 finiunmbl 24395 volfiniun 24398 iunmbl 24404 limciun 24745 iuneqfzuzlem 42487 fsumiunss 42734 sge0iunmpt 43574 meaiunincf 43639 meaiuninc3 43641 smfliminf 43979 dmmpossx2 45288 |
Copyright terms: Public domain | W3C validator |