Theorem cbviunv 4957

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

Syntax hints:   → wi 4   = wceq 1533  ∪ ciun 4911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-iun 4913

This theorem is referenced by:  iunxdif2  4969  otiunsndisj  5402  onfununi  7972  oelim2  8215  marypha2lem2  8894  trcl  9164  r1om  9660  fictb  9661  cfsmolem  9686  cfsmo  9687  domtriomlem  9858  domtriom  9859  pwfseq  10080  wunex2  10154  wuncval2  10163  fsuppmapnn0fiubex  13354  s3iunsndisj  14322  ackbijnn  15177  smndex1basss  18064  smndex1mgm  18066  efgs1b  18856  ablfaclem3  19203  ptbasfi  22183  bcth3  23928  itg1climres  24309  suppovss  30420  hashunif  30522  bnj601  32187  cvmliftlem15  32540  trpredlem1  33061  trpredtr  33064  trpredmintr  33065  trpredrec  33072  neibastop2  33704  filnetlem4  33724  sstotbnd2  35046  heiborlem3  35085  heibor  35093  lcfr  38715  mapdrval  38777  corclrcl  40045  trclrelexplem  40049  dftrcl3  40058  cotrcltrcl  40063  dfrtrcl3  40071  corcltrcl  40077  cotrclrcl  40080  ssmapsn  41472  cnrefiisplem  42103  cnrefiisp  42104  meaiuninclem  42756  meaiuninc  42757  meaiininc  42763  carageniuncllem2  42798  caratheodorylem1  42802  caratheodorylem2  42803  caratheodory  42804  ovnsubadd  42848  hoidmv1le  42870  hoidmvle  42876  ovnhoilem2  42878  hspmbl  42905  ovnovollem3  42934  vonvolmbl  42937  smflimlem2  43042  smflimlem3  43043  smflimlem4  43044  smflim  43047  smflim2  43074  smflimsup  43096  otiunsndisjX  43472