Theorem cbviunv 4966

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-11 2156  ax-12 2173  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ral 3068  df-rex 3069  df-iun 4923

This theorem is referenced by:  iunxdif2  4979  otiunsndisj  5428  onfununi  8143  oelim2  8388  marypha2lem2  9125  trpredlem1  9405  trpredtr  9408  trpredmintr  9409  trpredrec  9415  trcl  9417  r1om  9931  fictb  9932  cfsmolem  9957  cfsmo  9958  domtriomlem  10129  domtriom  10130  pwfseq  10351  wunex2  10425  wuncval2  10434  fsuppmapnn0fiubex  13640  s3iunsndisj  14607  ackbijnn  15468  smndex1basss  18459  smndex1mgm  18461  efgs1b  19257  ablfaclem3  19605  ptbasfi  22640  bcth3  24400  itg1climres  24784  suppovss  30919  hashunif  31028  bnj601  32800  cvmliftlem15  33160  ttrclselem1  33711  ttrclselem2  33712  neibastop2  34477  filnetlem4  34497  sstotbnd2  35859  heiborlem3  35898  heibor  35906  lcfr  39526  mapdrval  39588  corclrcl  41204  trclrelexplem  41208  dftrcl3  41217  cotrcltrcl  41222  dfrtrcl3  41230  corcltrcl  41236  cotrclrcl  41239  ssmapsn  42645  cnrefiisplem  43260  cnrefiisp  43261  meaiuninclem  43908  meaiuninc  43909  meaiininc  43915  carageniuncllem2  43950  caratheodorylem1  43954  caratheodorylem2  43955  caratheodory  43956  ovnsubadd  44000  hoidmv1le  44022  hoidmvle  44028  ovnhoilem2  44030  hspmbl  44057  ovnovollem3  44086  vonvolmbl  44089  smflimlem2  44194  smflimlem3  44195  smflimlem4  44196  smflim  44199  smflim2  44226  smflimsup  44248  otiunsndisjX  44658