| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbviunv | 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, 15-Sep-2003.) Add disjoint variable condition to avoid ax-13 2377. See cbviunvg 5042 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.) |
| Ref | Expression |
|---|---|
| cbviunv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
| Ref | Expression |
|---|---|
| cbviunv | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbviunv.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
| 2 | 1 | eleq2d 2827 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶)) |
| 3 | 2 | cbvrexvw 3238 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶) |
| 4 | 3 | abbii 2809 | . 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} |
| 5 | df-iun 4993 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} | |
| 6 | df-iun 4993 | . 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶} | |
| 7 | 4, 5, 6 | 3eqtr4i 2775 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 {cab 2714 ∃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-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rex 3071 df-iun 4993 |
| This theorem is referenced by: iunxdif2 5053 otiunsndisj 5525 onfununi 8381 oelim2 8633 marypha2lem2 9476 ttrclselem1 9765 ttrclselem2 9766 trcl 9768 r1om 10283 fictb 10284 cfsmolem 10310 cfsmo 10311 domtriomlem 10482 domtriom 10483 pwfseq 10704 wunex2 10778 wuncval2 10787 fsuppmapnn0fiubex 14033 s3iunsndisj 15007 ackbijnn 15864 smndex1basss 18918 smndex1mgm 18920 efgs1b 19754 ablfaclem3 20107 ptbasfi 23589 bcth3 25365 itg1climres 25749 suppovss 32690 hashunif 32810 gsumwrd2dccat 33070 fldextrspunlsplem 33723 bnj601 34934 cvmliftlem15 35303 neibastop2 36362 filnetlem4 36382 sstotbnd2 37781 heiborlem3 37820 heibor 37828 lcfr 41587 mapdrval 41649 corclrcl 43720 trclrelexplem 43724 dftrcl3 43733 cotrcltrcl 43738 dfrtrcl3 43746 corcltrcl 43752 cotrclrcl 43755 ssmapsn 45221 cnrefiisplem 45844 cnrefiisp 45845 meaiuninclem 46495 meaiuninc 46496 meaiininc 46502 carageniuncllem2 46537 caratheodorylem1 46541 caratheodorylem2 46542 caratheodory 46543 ovnsubadd 46587 hoidmv1le 46609 hoidmvle 46615 ovnhoilem2 46617 hspmbl 46644 ovnovollem3 46673 vonvolmbl 46676 smflimlem2 46787 smflimlem3 46788 smflimlem4 46789 smflim 46792 smflim2 46821 smflimsup 46843 otiunsndisjX 47291 |
| Copyright terms: Public domain | W3C validator |