Theorem cbviunv 5016

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 2376. See cbviunvg 5018 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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3221	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2802	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4969	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4969	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2768	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {cab 2713  ∃wrex 3060  ∪ ciun 4967

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rex 3061  df-iun 4969

This theorem is referenced by:  iunxdif2  5029  otiunsndisj  5495  onfununi  8355  oelim2  8607  marypha2lem2  9448  ttrclselem1  9739  ttrclselem2  9740  trcl  9742  r1om  10257  fictb  10258  cfsmolem  10284  cfsmo  10285  domtriomlem  10456  domtriom  10457  pwfseq  10678  wunex2  10752  wuncval2  10761  fsuppmapnn0fiubex  14010  s3iunsndisj  14987  ackbijnn  15844  smndex1basss  18883  smndex1mgm  18885  efgs1b  19717  ablfaclem3  20070  ptbasfi  23519  bcth3  25283  itg1climres  25667  suppovss  32658  hashunif  32785  gsumwrd2dccat  33061  fldextrspunlsplem  33714  bnj601  34951  cvmliftlem15  35320  neibastop2  36379  filnetlem4  36399  sstotbnd2  37798  heiborlem3  37837  heibor  37845  lcfr  41604  mapdrval  41666  corclrcl  43731  trclrelexplem  43735  dftrcl3  43744  cotrcltrcl  43749  dfrtrcl3  43757  corcltrcl  43763  cotrclrcl  43766  ssmapsn  45240  cnrefiisplem  45858  cnrefiisp  45859  meaiuninclem  46509  meaiuninc  46510  meaiininc  46516  carageniuncllem2  46551  caratheodorylem1  46555  caratheodorylem2  46556  caratheodory  46557  ovnsubadd  46601  hoidmv1le  46623  hoidmvle  46629  ovnhoilem2  46631  hspmbl  46658  ovnovollem3  46687  vonvolmbl  46690  smflimlem2  46801  smflimlem3  46802  smflimlem4  46803  smflim  46806  smflim2  46835  smflimsup  46857  otiunsndisjX  47308