Theorem cbviunv 4968

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 4970 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 2825	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3218	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2806	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4923	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4923	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2772	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {cab 2717  ∃wrex 3063  ∪ ciun 4921

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rex 3064  df-iun 4923

This theorem is referenced by:  iunxdif2  4983  otiunsndisj  5461  onfununi  8271  oelim2  8521  marypha2lem2  9339  ttrclselem1  9637  ttrclselem2  9638  trcl  9640  r1om  10156  fictb  10157  cfsmolem  10183  cfsmo  10184  domtriomlem  10355  domtriom  10356  pwfseq  10578  wunex2  10652  wuncval2  10661  fsuppmapnn0fiubex  13945  s3iunsndisj  14921  ackbijnn  15784  smndex1basss  18867  smndex1mgm  18869  efgs1b  19702  ablfaclem3  20055  ptbasfi  23564  bcth3  25316  itg1climres  25699  suppovss  32773  hashunif  32898  gsumwrd2dccat  33159  fldextrspunlsplem  33857  bnj601  35102  cvmliftlem15  35526  neibastop2  36589  filnetlem4  36609  sstotbnd2  38141  heiborlem3  38180  heibor  38188  lcfr  42077  mapdrval  42139  corclrcl  44151  trclrelexplem  44155  dftrcl3  44164  cotrcltrcl  44169  dfrtrcl3  44177  corcltrcl  44183  cotrclrcl  44186  ssmapsn  45661  cnrefiisplem  46272  cnrefiisp  46273  meaiuninclem  46923  meaiuninc  46924  meaiininc  46930  carageniuncllem2  46965  caratheodorylem1  46969  caratheodorylem2  46970  caratheodory  46971  ovnsubadd  47015  hoidmv1le  47037  hoidmvle  47043  ovnhoilem2  47045  hspmbl  47072  ovnovollem3  47101  vonvolmbl  47104  smflimlem2  47215  smflimlem3  47216  smflimlem4  47217  smflim  47220  smflim2  47249  smflimsup  47271  otiunsndisjX  47742