Theorem cbviunv 5002

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 2404. See cbviunvg 5004 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 2850	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3245	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2830	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4958	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4958	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2796	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  ∪ ciun 4956

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rex 3091  df-iun 4958

This theorem is used by:  iunxdif2  5017  otiunsndisj  5500  onfununi  8387  oelim2  8642  marypha2lem2  9465  ttrclselem1  9763  ttrclselem2  9764  trcl  9766  hfom  10360  fictb  10361  cfsmolem  10387  cfsmo  10388  domtriomlem  10559  domtriom  10560  pwfseq  10788  wunex2  10862  wuncval2  10871  fsuppmapnn0fiubex  14175  s3iunsndisj  15164  ackbijnn  16041  smndex1basss  19154  smndex1mgm  19156  efgs1b  20001  ablfaclem3  20354  ptbasfi  23955  bcth3  25707  itg1climres  26090  suppovss  33371  hashunif  33494  gsumwrd2dccat  33738  fldextrspunlsplem  34416  bnj601  35661  cvmliftlem15  36271  neibastop2  37364  filnetlem4  37384  sstotbnd2  38974  heiborlem3  39013  heibor  39021  lcfr  42908  mapdrval  42970  corclrcl  44968  trclrelexplem  44972  dftrcl3  44981  cotrcltrcl  44986  dfrtrcl3  44994  corcltrcl  45000  cotrclrcl  45003  ackbij3  46289  ssmapsn  46502  cnrefiisplem  47112  cnrefiisp  47113  meaiuninclem  47763  meaiuninc  47764  meaiininc  47770  carageniuncllem2  47805  caratheodorylem1  47809  caratheodorylem2  47810  caratheodory  47811  ovnsubadd  47855  hoidmv1le  47877  hoidmvle  47883  ovnhoilem2  47885  hspmbl  47912  ovnovollem3  47941  vonvolmbl  47944  smflimlem2  48055  smflimlem3  48056  smflimlem4  48057  smflim  48060  smflim2  48089  smflimsup  48111  otiunsndisjX  48622