Theorem cbviunv 4987

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 2372. See cbviunvg 4989 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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3211	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2798	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4941	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4941	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2764	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {cab 2709  ∃wrex 3056  ∪ ciun 4939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rex 3057  df-iun 4941

This theorem is referenced by:  iunxdif2  5000  otiunsndisj  5458  onfununi  8261  oelim2  8510  marypha2lem2  9320  ttrclselem1  9615  ttrclselem2  9616  trcl  9618  r1om  10134  fictb  10135  cfsmolem  10161  cfsmo  10162  domtriomlem  10333  domtriom  10334  pwfseq  10555  wunex2  10629  wuncval2  10638  fsuppmapnn0fiubex  13899  s3iunsndisj  14875  ackbijnn  15735  smndex1basss  18813  smndex1mgm  18815  efgs1b  19648  ablfaclem3  20001  ptbasfi  23496  bcth3  25258  itg1climres  25642  suppovss  32662  hashunif  32788  gsumwrd2dccat  33047  fldextrspunlsplem  33686  bnj601  34932  cvmliftlem15  35342  neibastop2  36403  filnetlem4  36423  sstotbnd2  37822  heiborlem3  37861  heibor  37869  lcfr  41632  mapdrval  41694  corclrcl  43748  trclrelexplem  43752  dftrcl3  43761  cotrcltrcl  43766  dfrtrcl3  43774  corcltrcl  43780  cotrclrcl  43783  ssmapsn  45261  cnrefiisplem  45875  cnrefiisp  45876  meaiuninclem  46526  meaiuninc  46527  meaiininc  46533  carageniuncllem2  46568  caratheodorylem1  46572  caratheodorylem2  46573  caratheodory  46574  ovnsubadd  46618  hoidmv1le  46640  hoidmvle  46646  ovnhoilem2  46648  hspmbl  46675  ovnovollem3  46704  vonvolmbl  46707  smflimlem2  46818  smflimlem3  46819  smflimlem4  46820  smflim  46823  smflim2  46852  smflimsup  46874  otiunsndisjX  47318