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.) |
Ref | Expression |
---|---|
cbviunv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbviunv | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2751 | . 2 ⊢ Ⅎ𝑦𝐵 | |
2 | nfcv 2751 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | cbviunv.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
4 | 1, 2, 3 | cbviun 4493 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 ∪ ciun 4455 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-iun 4457 |
This theorem is referenced by: iunxdif2 4504 otiunsndisj 4905 onfununi 7325 oelim2 7562 marypha2lem2 8225 trcl 8487 r1om 8949 fictb 8950 cfsmolem 8975 cfsmo 8976 domtriomlem 9147 domtriom 9148 pwfseq 9365 wunex2 9439 wuncval2 9448 fsuppmapnn0fiubex 12654 s3iunsndisj 13555 ackbijnn 14399 efgs1b 17972 ablfaclem3 18309 ptbasfi 21194 bcth3 22936 itg1climres 23287 2spotiundisj 26589 hashunif 28949 bnj601 30244 cvmliftlem15 30534 trpredlem1 30971 trpredtr 30974 trpredmintr 30975 trpredrec 30982 neibastop2 31526 filnetlem4 31546 sstotbnd2 32743 heiborlem3 32782 heibor 32790 lcfr 35892 mapdrval 35954 corclrcl 37018 trclrelexplem 37022 dftrcl3 37031 cotrcltrcl 37036 dfrtrcl3 37044 corcltrcl 37050 cotrclrcl 37053 ssmapsn 38403 meaiuninclem 39373 meaiuninc 39374 meaiininc 39377 carageniuncllem2 39412 caratheodorylem1 39416 caratheodorylem2 39417 caratheodory 39418 ovnsubadd 39462 hoidmv1le 39484 hoidmvle 39490 ovnhoilem2 39492 hspmbl 39519 ovnovollem3 39548 vonvolmbl 39551 smflimlem2 39658 smflimlem3 39659 smflimlem4 39660 smflim 39663 otiunsndisjX 40317 2wspiundisj 41166 |
Copyright terms: Public domain | W3C validator |