Theorem cbviunv 5063

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 2380. See cbviunvg 5065 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 2830	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3244	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2812	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 5017	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 5017	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2778	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {cab 2717  ∃wrex 3076  ∪ ciun 5015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rex 3077  df-iun 5017

This theorem is referenced by:  iunxdif2  5076  otiunsndisj  5539  onfununi  8397  oelim2  8651  marypha2lem2  9505  ttrclselem1  9794  ttrclselem2  9795  trcl  9797  r1om  10312  fictb  10313  cfsmolem  10339  cfsmo  10340  domtriomlem  10511  domtriom  10512  pwfseq  10733  wunex2  10807  wuncval2  10816  fsuppmapnn0fiubex  14043  s3iunsndisj  15017  ackbijnn  15876  smndex1basss  18940  smndex1mgm  18942  efgs1b  19778  ablfaclem3  20131  ptbasfi  23610  bcth3  25384  itg1climres  25769  suppovss  32697  hashunif  32813  bnj601  34896  cvmliftlem15  35266  neibastop2  36327  filnetlem4  36347  sstotbnd2  37734  heiborlem3  37773  heibor  37781  lcfr  41542  mapdrval  41604  corclrcl  43669  trclrelexplem  43673  dftrcl3  43682  cotrcltrcl  43687  dfrtrcl3  43695  corcltrcl  43701  cotrclrcl  43704  ssmapsn  45123  cnrefiisplem  45750  cnrefiisp  45751  meaiuninclem  46401  meaiuninc  46402  meaiininc  46408  carageniuncllem2  46443  caratheodorylem1  46447  caratheodorylem2  46448  caratheodory  46449  ovnsubadd  46493  hoidmv1le  46515  hoidmvle  46521  ovnhoilem2  46523  hspmbl  46550  ovnovollem3  46579  vonvolmbl  46582  smflimlem2  46693  smflimlem3  46694  smflimlem4  46695  smflim  46698  smflim2  46727  smflimsup  46749  otiunsndisjX  47194