Theorem cbviunv 4970

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 2372. See cbviunvg 4972 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 2907	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2907	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 4966	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1539  ∪ ciun 4924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-iun 4926

This theorem is referenced by:  iunxdif2  4983  otiunsndisj  5434  onfununi  8172  oelim2  8426  marypha2lem2  9195  ttrclselem1  9483  ttrclselem2  9484  trcl  9486  r1om  10000  fictb  10001  cfsmolem  10026  cfsmo  10027  domtriomlem  10198  domtriom  10199  pwfseq  10420  wunex2  10494  wuncval2  10503  fsuppmapnn0fiubex  13712  s3iunsndisj  14679  ackbijnn  15540  smndex1basss  18544  smndex1mgm  18546  efgs1b  19342  ablfaclem3  19690  ptbasfi  22732  bcth3  24495  itg1climres  24879  suppovss  31017  hashunif  31126  bnj601  32900  cvmliftlem15  33260  neibastop2  34550  filnetlem4  34570  sstotbnd2  35932  heiborlem3  35971  heibor  35979  lcfr  39599  mapdrval  39661  corclrcl  41315  trclrelexplem  41319  dftrcl3  41328  cotrcltrcl  41333  dfrtrcl3  41341  corcltrcl  41347  cotrclrcl  41350  ssmapsn  42756  cnrefiisplem  43370  cnrefiisp  43371  meaiuninclem  44018  meaiuninc  44019  meaiininc  44025  carageniuncllem2  44060  caratheodorylem1  44064  caratheodorylem2  44065  caratheodory  44066  ovnsubadd  44110  hoidmv1le  44132  hoidmvle  44138  ovnhoilem2  44140  hspmbl  44167  ovnovollem3  44196  vonvolmbl  44199  smflimlem2  44307  smflimlem3  44308  smflimlem4  44309  smflim  44312  smflim2  44339  smflimsup  44361  otiunsndisjX  44771