Theorem cbviunv 5045

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 2375. See cbviunvg 5047 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 3236	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2807	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4998	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4998	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2773	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2106  {cab 2712  ∃wrex 3068  ∪ ciun 4996

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rex 3069  df-iun 4998

This theorem is referenced by:  iunxdif2  5058  otiunsndisj  5530  onfununi  8380  oelim2  8632  marypha2lem2  9474  ttrclselem1  9763  ttrclselem2  9764  trcl  9766  r1om  10281  fictb  10282  cfsmolem  10308  cfsmo  10309  domtriomlem  10480  domtriom  10481  pwfseq  10702  wunex2  10776  wuncval2  10785  fsuppmapnn0fiubex  14030  s3iunsndisj  15004  ackbijnn  15861  smndex1basss  18931  smndex1mgm  18933  efgs1b  19769  ablfaclem3  20122  ptbasfi  23605  bcth3  25379  itg1climres  25764  suppovss  32696  hashunif  32816  gsumwrd2dccat  33053  bnj601  34913  cvmliftlem15  35283  neibastop2  36344  filnetlem4  36364  sstotbnd2  37761  heiborlem3  37800  heibor  37808  lcfr  41568  mapdrval  41630  corclrcl  43697  trclrelexplem  43701  dftrcl3  43710  cotrcltrcl  43715  dfrtrcl3  43723  corcltrcl  43729  cotrclrcl  43732  ssmapsn  45159  cnrefiisplem  45785  cnrefiisp  45786  meaiuninclem  46436  meaiuninc  46437  meaiininc  46443  carageniuncllem2  46478  caratheodorylem1  46482  caratheodorylem2  46483  caratheodory  46484  ovnsubadd  46528  hoidmv1le  46550  hoidmvle  46556  ovnhoilem2  46558  hspmbl  46585  ovnovollem3  46614  vonvolmbl  46617  smflimlem2  46728  smflimlem3  46729  smflimlem4  46730  smflim  46733  smflim2  46762  smflimsup  46784  otiunsndisjX  47229