![]() |
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 2371. See cbviunvg 5044 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.) |
Ref | Expression |
---|---|
cbviunv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbviunv | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2903 | . 2 ⊢ Ⅎ𝑦𝐵 | |
2 | nfcv 2903 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | cbviunv.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
4 | 1, 2, 3 | cbviun 5038 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∪ ciun 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-11 2154 ax-12 2171 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ral 3062 df-rex 3071 df-iun 4998 |
This theorem is referenced by: iunxdif2 5055 otiunsndisj 5519 onfununi 8337 oelim2 8591 marypha2lem2 9427 ttrclselem1 9716 ttrclselem2 9717 trcl 9719 r1om 10235 fictb 10236 cfsmolem 10261 cfsmo 10262 domtriomlem 10433 domtriom 10434 pwfseq 10655 wunex2 10729 wuncval2 10738 fsuppmapnn0fiubex 13953 s3iunsndisj 14911 ackbijnn 15770 smndex1basss 18782 smndex1mgm 18784 efgs1b 19598 ablfaclem3 19951 ptbasfi 23076 bcth3 24839 itg1climres 25223 suppovss 31893 hashunif 32005 bnj601 33919 cvmliftlem15 34277 neibastop2 35234 filnetlem4 35254 sstotbnd2 36630 heiborlem3 36669 heibor 36677 lcfr 40444 mapdrval 40506 corclrcl 42443 trclrelexplem 42447 dftrcl3 42456 cotrcltrcl 42461 dfrtrcl3 42469 corcltrcl 42475 cotrclrcl 42478 ssmapsn 43900 cnrefiisplem 44531 cnrefiisp 44532 meaiuninclem 45182 meaiuninc 45183 meaiininc 45189 carageniuncllem2 45224 caratheodorylem1 45228 caratheodorylem2 45229 caratheodory 45230 ovnsubadd 45274 hoidmv1le 45296 hoidmvle 45302 ovnhoilem2 45304 hspmbl 45331 ovnovollem3 45360 vonvolmbl 45363 smflimlem2 45474 smflimlem3 45475 smflimlem4 45476 smflim 45479 smflim2 45508 smflimsup 45530 otiunsndisjX 45973 |
Copyright terms: Public domain | W3C validator |