Theorem cbviunv 4982

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 4984 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 2823	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3217	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2804	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4936	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4936	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2770	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3062  ∪ ciun 4934

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-iun 4936

This theorem is referenced by:  iunxdif2  4997  otiunsndisj  5469  onfununi  8275  oelim2  8525  marypha2lem2  9343  ttrclselem1  9640  ttrclselem2  9641  trcl  9643  r1om  10159  fictb  10160  cfsmolem  10186  cfsmo  10187  domtriomlem  10358  domtriom  10359  pwfseq  10581  wunex2  10655  wuncval2  10664  fsuppmapnn0fiubex  13948  s3iunsndisj  14924  ackbijnn  15787  smndex1basss  18870  smndex1mgm  18872  efgs1b  19705  ablfaclem3  20058  ptbasfi  23559  bcth3  25311  itg1climres  25694  suppovss  32772  hashunif  32897  gsumwrd2dccat  33157  fldextrspunlsplem  33836  bnj601  35081  cvmliftlem15  35499  neibastop2  36562  filnetlem4  36582  sstotbnd2  38112  heiborlem3  38151  heibor  38159  lcfr  42048  mapdrval  42110  corclrcl  44155  trclrelexplem  44159  dftrcl3  44168  cotrcltrcl  44173  dfrtrcl3  44181  corcltrcl  44187  cotrclrcl  44190  ssmapsn  45666  cnrefiisplem  46278  cnrefiisp  46279  meaiuninclem  46929  meaiuninc  46930  meaiininc  46936  carageniuncllem2  46971  caratheodorylem1  46975  caratheodorylem2  46976  caratheodory  46977  ovnsubadd  47021  hoidmv1le  47043  hoidmvle  47049  ovnhoilem2  47051  hspmbl  47078  ovnovollem3  47107  vonvolmbl  47110  smflimlem2  47221  smflimlem3  47222  smflimlem4  47223  smflim  47226  smflim2  47255  smflimsup  47277  otiunsndisjX  47742