Theorem cbviunv 5042

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.)

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 2903	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2903	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 5038	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

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