Theorem cbviunv 5040

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 2377. See cbviunvg 5042 for a less restrictive version requiring more axioms. (Revised by GG, 14-Aug-2025.)

Hypothesis

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

Assertion

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

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

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

Proof of Theorem cbviunv

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cbviunv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
2	1	eleq2d 2827	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3238	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2809	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4993	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4993	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2775	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2714  ∃wrex 3070  ∪ ciun 4991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rex 3071  df-iun 4993

This theorem is referenced by:  iunxdif2  5053  otiunsndisj  5525  onfununi  8381  oelim2  8633  marypha2lem2  9476  ttrclselem1  9765  ttrclselem2  9766  trcl  9768  r1om  10283  fictb  10284  cfsmolem  10310  cfsmo  10311  domtriomlem  10482  domtriom  10483  pwfseq  10704  wunex2  10778  wuncval2  10787  fsuppmapnn0fiubex  14033  s3iunsndisj  15007  ackbijnn  15864  smndex1basss  18918  smndex1mgm  18920  efgs1b  19754  ablfaclem3  20107  ptbasfi  23589  bcth3  25365  itg1climres  25749  suppovss  32690  hashunif  32810  gsumwrd2dccat  33070  fldextrspunlsplem  33723  bnj601  34934  cvmliftlem15  35303  neibastop2  36362  filnetlem4  36382  sstotbnd2  37781  heiborlem3  37820  heibor  37828  lcfr  41587  mapdrval  41649  corclrcl  43720  trclrelexplem  43724  dftrcl3  43733  cotrcltrcl  43738  dfrtrcl3  43746  corcltrcl  43752  cotrclrcl  43755  ssmapsn  45221  cnrefiisplem  45844  cnrefiisp  45845  meaiuninclem  46495  meaiuninc  46496  meaiininc  46502  carageniuncllem2  46537  caratheodorylem1  46541  caratheodorylem2  46542  caratheodory  46543  ovnsubadd  46587  hoidmv1le  46609  hoidmvle  46615  ovnhoilem2  46617  hspmbl  46644  ovnovollem3  46673  vonvolmbl  46676  smflimlem2  46787  smflimlem3  46788  smflimlem4  46789  smflim  46792  smflim2  46821  smflimsup  46843  otiunsndisjX  47291