Theorem cbviunv 4994

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 2376. See cbviunvg 4996 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 2822	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3215	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2803	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4948	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4948	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2769	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {cab 2714  ∃wrex 3060  ∪ ciun 4946

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 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-iun 4948

This theorem is referenced by:  iunxdif2  5009  otiunsndisj  5468  onfununi  8273  oelim2  8523  marypha2lem2  9339  ttrclselem1  9634  ttrclselem2  9635  trcl  9637  r1om  10153  fictb  10154  cfsmolem  10180  cfsmo  10181  domtriomlem  10352  domtriom  10353  pwfseq  10575  wunex2  10649  wuncval2  10658  fsuppmapnn0fiubex  13915  s3iunsndisj  14891  ackbijnn  15751  smndex1basss  18830  smndex1mgm  18832  efgs1b  19665  ablfaclem3  20018  ptbasfi  23525  bcth3  25287  itg1climres  25671  suppovss  32760  hashunif  32886  gsumwrd2dccat  33160  fldextrspunlsplem  33830  bnj601  35076  cvmliftlem15  35492  neibastop2  36555  filnetlem4  36575  sstotbnd2  37975  heiborlem3  38014  heibor  38022  lcfr  41845  mapdrval  41907  corclrcl  43948  trclrelexplem  43952  dftrcl3  43961  cotrcltrcl  43966  dfrtrcl3  43974  corcltrcl  43980  cotrclrcl  43983  ssmapsn  45460  cnrefiisplem  46073  cnrefiisp  46074  meaiuninclem  46724  meaiuninc  46725  meaiininc  46731  carageniuncllem2  46766  caratheodorylem1  46770  caratheodorylem2  46771  caratheodory  46772  ovnsubadd  46816  hoidmv1le  46838  hoidmvle  46844  ovnhoilem2  46846  hspmbl  46873  ovnovollem3  46902  vonvolmbl  46905  smflimlem2  47016  smflimlem3  47017  smflimlem4  47018  smflim  47021  smflim2  47050  smflimsup  47072  otiunsndisjX  47525