Theorem cbviunv 5004

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 2370. See cbviunvg 5006 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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3216	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2796	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4957	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4957	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  ∪ ciun 4955

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-iun 4957

This theorem is referenced by:  iunxdif2  5017  otiunsndisj  5480  onfununi  8310  oelim2  8559  marypha2lem2  9387  ttrclselem1  9678  ttrclselem2  9679  trcl  9681  r1om  10196  fictb  10197  cfsmolem  10223  cfsmo  10224  domtriomlem  10395  domtriom  10396  pwfseq  10617  wunex2  10691  wuncval2  10700  fsuppmapnn0fiubex  13957  s3iunsndisj  14934  ackbijnn  15794  smndex1basss  18832  smndex1mgm  18834  efgs1b  19666  ablfaclem3  20019  ptbasfi  23468  bcth3  25231  itg1climres  25615  suppovss  32604  hashunif  32731  gsumwrd2dccat  33007  fldextrspunlsplem  33668  bnj601  34910  cvmliftlem15  35285  neibastop2  36349  filnetlem4  36369  sstotbnd2  37768  heiborlem3  37807  heibor  37815  lcfr  41579  mapdrval  41641  corclrcl  43696  trclrelexplem  43700  dftrcl3  43709  cotrcltrcl  43714  dfrtrcl3  43722  corcltrcl  43728  cotrclrcl  43731  ssmapsn  45210  cnrefiisplem  45827  cnrefiisp  45828  meaiuninclem  46478  meaiuninc  46479  meaiininc  46485  carageniuncllem2  46520  caratheodorylem1  46524  caratheodorylem2  46525  caratheodory  46526  ovnsubadd  46570  hoidmv1le  46592  hoidmvle  46598  ovnhoilem2  46600  hspmbl  46627  ovnovollem3  46656  vonvolmbl  46659  smflimlem2  46770  smflimlem3  46771  smflimlem4  46772  smflim  46775  smflim2  46804  smflimsup  46826  otiunsndisjX  47280