Theorem cbviunv 5007

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 2371. See cbviunvg 5009 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 2815	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3217	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2797	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4960	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4960	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2763	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2708  ∃wrex 3054  ∪ ciun 4958

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rex 3055  df-iun 4960

This theorem is referenced by:  iunxdif2  5020  otiunsndisj  5483  onfununi  8313  oelim2  8562  marypha2lem2  9394  ttrclselem1  9685  ttrclselem2  9686  trcl  9688  r1om  10203  fictb  10204  cfsmolem  10230  cfsmo  10231  domtriomlem  10402  domtriom  10403  pwfseq  10624  wunex2  10698  wuncval2  10707  fsuppmapnn0fiubex  13964  s3iunsndisj  14941  ackbijnn  15801  smndex1basss  18839  smndex1mgm  18841  efgs1b  19673  ablfaclem3  20026  ptbasfi  23475  bcth3  25238  itg1climres  25622  suppovss  32611  hashunif  32738  gsumwrd2dccat  33014  fldextrspunlsplem  33675  bnj601  34917  cvmliftlem15  35292  neibastop2  36356  filnetlem4  36376  sstotbnd2  37775  heiborlem3  37814  heibor  37822  lcfr  41586  mapdrval  41648  corclrcl  43703  trclrelexplem  43707  dftrcl3  43716  cotrcltrcl  43721  dfrtrcl3  43729  corcltrcl  43735  cotrclrcl  43738  ssmapsn  45217  cnrefiisplem  45834  cnrefiisp  45835  meaiuninclem  46485  meaiuninc  46486  meaiininc  46492  carageniuncllem2  46527  caratheodorylem1  46531  caratheodorylem2  46532  caratheodory  46533  ovnsubadd  46577  hoidmv1le  46599  hoidmvle  46605  ovnhoilem2  46607  hspmbl  46634  ovnovollem3  46663  vonvolmbl  46666  smflimlem2  46777  smflimlem3  46778  smflimlem4  46779  smflim  46782  smflim2  46811  smflimsup  46833  otiunsndisjX  47284