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  18808  smndex1mgm  18810  efgs1b  19642  ablfaclem3  19995  ptbasfi  23444  bcth3  25207  itg1climres  25591  suppovss  32577  hashunif  32704  gsumwrd2dccat  32980  fldextrspunlsplem  33641  bnj601  34883  cvmliftlem15  35258  neibastop2  36322  filnetlem4  36342  sstotbnd2  37741  heiborlem3  37780  heibor  37788  lcfr  41552  mapdrval  41614  corclrcl  43669  trclrelexplem  43673  dftrcl3  43682  cotrcltrcl  43687  dfrtrcl3  43695  corcltrcl  43701  cotrclrcl  43704  ssmapsn  45183  cnrefiisplem  45800  cnrefiisp  45801  meaiuninclem  46451  meaiuninc  46452  meaiininc  46458  carageniuncllem2  46493  caratheodorylem1  46497  caratheodorylem2  46498  caratheodory  46499  ovnsubadd  46543  hoidmv1le  46565  hoidmvle  46571  ovnhoilem2  46573  hspmbl  46600  ovnovollem3  46629  vonvolmbl  46632  smflimlem2  46743  smflimlem3  46744  smflimlem4  46745  smflim  46748  smflim2  46777  smflimsup  46799  otiunsndisjX  47253