Theorem cbviunv 4999

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 2370. See cbviunvg 5001 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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3214	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2796	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4953	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4953	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  ∪ ciun 4951

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-iun 4953

This theorem is referenced by:  iunxdif2  5012  otiunsndisj  5475  onfununi  8287  oelim2  8536  marypha2lem2  9363  ttrclselem1  9654  ttrclselem2  9655  trcl  9657  r1om  10172  fictb  10173  cfsmolem  10199  cfsmo  10200  domtriomlem  10371  domtriom  10372  pwfseq  10593  wunex2  10667  wuncval2  10676  fsuppmapnn0fiubex  13933  s3iunsndisj  14910  ackbijnn  15770  smndex1basss  18814  smndex1mgm  18816  efgs1b  19650  ablfaclem3  20003  ptbasfi  23501  bcth3  25264  itg1climres  25648  suppovss  32654  hashunif  32781  gsumwrd2dccat  33050  fldextrspunlsplem  33661  bnj601  34903  cvmliftlem15  35278  neibastop2  36342  filnetlem4  36362  sstotbnd2  37761  heiborlem3  37800  heibor  37808  lcfr  41572  mapdrval  41634  corclrcl  43689  trclrelexplem  43693  dftrcl3  43702  cotrcltrcl  43707  dfrtrcl3  43715  corcltrcl  43721  cotrclrcl  43724  ssmapsn  45203  cnrefiisplem  45820  cnrefiisp  45821  meaiuninclem  46471  meaiuninc  46472  meaiininc  46478  carageniuncllem2  46513  caratheodorylem1  46517  caratheodorylem2  46518  caratheodory  46519  ovnsubadd  46563  hoidmv1le  46585  hoidmvle  46591  ovnhoilem2  46593  hspmbl  46620  ovnovollem3  46649  vonvolmbl  46652  smflimlem2  46763  smflimlem3  46764  smflimlem4  46765  smflim  46768  smflim2  46797  smflimsup  46819  otiunsndisjX  47273