Theorem cbviunv 5005

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 2406. See cbviunvg 5007 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 2851	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3246	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2832	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4960	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4960	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2798	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {cab 2743  ∃wrex 3091  ∪ ciun 4958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rex 3092  df-iun 4960

This theorem is used by:  iunxdif2  5020  otiunsndisj  5505  onfununi  8334  oelim2  8587  marypha2lem2  9403  ttrclselem1  9701  ttrclselem2  9702  trcl  9704  r1om  10242  fictb  10243  cfsmolem  10269  cfsmo  10270  domtriomlem  10441  domtriom  10442  pwfseq  10664  wunex2  10738  wuncval2  10747  fsuppmapnn0fiubex  14046  s3iunsndisj  15029  ackbijnn  15905  smndex1basss  19004  smndex1mgm  19006  efgs1b  19850  ablfaclem3  20203  ptbasfi  23789  bcth3  25541  itg1climres  25924  suppovss  33097  hashunif  33221  gsumwrd2dccat  33462  fldextrspunlsplem  34127  bnj601  35373  cvmliftlem15  35827  neibastop2  36929  filnetlem4  36949  sstotbnd2  38483  heiborlem3  38522  heibor  38530  lcfr  42417  mapdrval  42479  corclrcl  44491  trclrelexplem  44495  dftrcl3  44504  cotrcltrcl  44509  dfrtrcl3  44517  corcltrcl  44523  cotrclrcl  44526  ssmapsn  45990  cnrefiisplem  46601  cnrefiisp  46602  meaiuninclem  47252  meaiuninc  47253  meaiininc  47259  carageniuncllem2  47294  caratheodorylem1  47298  caratheodorylem2  47299  caratheodory  47300  ovnsubadd  47344  hoidmv1le  47366  hoidmvle  47372  ovnhoilem2  47374  hspmbl  47401  ovnovollem3  47430  vonvolmbl  47433  smflimlem2  47544  smflimlem3  47545  smflimlem4  47546  smflim  47549  smflim2  47578  smflimsup  47600  otiunsndisjX  48074