![]() |
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.) |
Ref | Expression |
---|---|
cbviun.1 | ⊢ Ⅎ𝑦𝐵 |
cbviun.2 | ⊢ Ⅎ𝑥𝐶 |
cbviun.3 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbviun | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cbviun.1 | . . . . 5 ⊢ Ⅎ𝑦𝐵 | |
2 | 1 | nfcri 2945 | . . . 4 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐵 |
3 | cbviun.2 | . . . . 5 ⊢ Ⅎ𝑥𝐶 | |
4 | 3 | nfcri 2945 | . . . 4 ⊢ Ⅎ𝑥 𝑧 ∈ 𝐶 |
5 | cbviun.3 | . . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
6 | 5 | eleq2d 2870 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
7 | 2, 4, 6 | cbvrex 3402 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶) |
8 | 7 | abbii 2863 | . 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} |
9 | df-iun 4833 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
10 | df-iun 4833 | . 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} | |
11 | 8, 9, 10 | 3eqtr4i 2831 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1525 ∈ wcel 2083 {cab 2777 Ⅎwnfc 2935 ∃wrex 3108 ∪ ciun 4831 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ral 3112 df-rex 3113 df-iun 4833 |
This theorem is referenced by: cbviunv 4872 disjxiun 4965 funiunfvf 6880 mpomptsx 7625 dmmpossx 7627 fmpox 7628 ovmptss 7651 iunfi 8665 fsum2dlem 14962 fsumcom2 14966 fsumiun 15013 fprod2dlem 15171 fprodcom2 15175 gsumcom2 18819 fiuncmp 21700 ovolfiniun 23789 ovoliunlem3 23792 ovoliun 23793 finiunmbl 23832 volfiniun 23835 iunmbl 23841 limciun 24179 iuneqfzuzlem 41164 fsumiunss 41419 sge0iunmpt 42264 meaiunincf 42329 meaiuninc3 42331 smfliminf 42669 dmmpossx2 43885 |
Copyright terms: Public domain | W3C validator |