Theorem cbviunv 5007

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 2410. See cbviunvg 5009 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 2855	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3250	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2836	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4962	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4962	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2802	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1567   ∈ wcel 2149  {cab 2747  ∃wrex 3095  ∪ ciun 4960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rex 3096  df-iun 4962

This theorem is referenced by:  iunxdif2  5022  otiunsndisj  5504  onfununi  8327  oelim2  8580  marypha2lem2  9395  ttrclselem1  9693  ttrclselem2  9694  trcl  9696  r1om  10225  fictb  10226  cfsmolem  10253  cfsmo  10254  domtriomlem  10425  domtriom  10426  pwfseq  10648  wunex2  10722  wuncval2  10731  fsuppmapnn0fiubex  14027  s3iunsndisj  15004  ackbijnn  15881  smndex1basss  18966  smndex1mgm  18968  efgs1b  19805  ablfaclem3  20158  ptbasfi  23706  bcth3  25458  itg1climres  25841  suppovss  32966  hashunif  33091  gsumwrd2dccat  33338  fldextrspunlsplem  34007  bnj601  35252  cvmliftlem15  35688  neibastop2  36760  filnetlem4  36780  sstotbnd2  38312  heiborlem3  38351  heibor  38359  lcfr  42248  mapdrval  42310  corclrcl  44324  trclrelexplem  44328  dftrcl3  44337  cotrcltrcl  44342  dfrtrcl3  44350  corcltrcl  44356  cotrclrcl  44359  ssmapsn  45823  cnrefiisplem  46434  cnrefiisp  46435  meaiuninclem  47085  meaiuninc  47086  meaiininc  47092  carageniuncllem2  47127  caratheodorylem1  47131  caratheodorylem2  47132  caratheodory  47133  ovnsubadd  47177  hoidmv1le  47199  hoidmvle  47205  ovnhoilem2  47207  hspmbl  47234  ovnovollem3  47263  vonvolmbl  47266  smflimlem2  47377  smflimlem3  47378  smflimlem4  47379  smflim  47382  smflim2  47411  smflimsup  47433  otiunsndisjX  47904