Theorem cbviunv 4935

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 4937 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)

Hypothesis

Ref	Expression
cbviunv.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbviunv	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbviunv

Step	Hyp	Ref	Expression
1		nfcv 2897	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2897	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 4931	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1543  ∪ 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:  iunxdif2  4948  otiunsndisj  5388  onfununi  8056  oelim2  8301  marypha2lem2  9030  trpredlem1  9310  trpredtr  9313  trpredmintr  9314  trpredrec  9320  trcl  9322  r1om  9823  fictb  9824  cfsmolem  9849  cfsmo  9850  domtriomlem  10021  domtriom  10022  pwfseq  10243  wunex2  10317  wuncval2  10326  fsuppmapnn0fiubex  13530  s3iunsndisj  14496  ackbijnn  15355  smndex1basss  18286  smndex1mgm  18288  efgs1b  19080  ablfaclem3  19428  ptbasfi  22432  bcth3  24182  itg1climres  24566  suppovss  30691  hashunif  30800  bnj601  32567  cvmliftlem15  32927  neibastop2  34236  filnetlem4  34256  sstotbnd2  35618  heiborlem3  35657  heibor  35665  lcfr  39285  mapdrval  39347  corclrcl  40933  trclrelexplem  40937  dftrcl3  40946  cotrcltrcl  40951  dfrtrcl3  40959  corcltrcl  40965  cotrclrcl  40968  ssmapsn  42370  cnrefiisplem  42988  cnrefiisp  42989  meaiuninclem  43636  meaiuninc  43637  meaiininc  43643  carageniuncllem2  43678  caratheodorylem1  43682  caratheodorylem2  43683  caratheodory  43684  ovnsubadd  43728  hoidmv1le  43750  hoidmvle  43756  ovnhoilem2  43758  hspmbl  43785  ovnovollem3  43814  vonvolmbl  43817  smflimlem2  43922  smflimlem3  43923  smflimlem4  43924  smflim  43927  smflim2  43954  smflimsup  43976  otiunsndisjX  44386