Theorem cbviunv 5008

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 2407. See cbviunvg 5010 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 2852	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3247	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2833	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4963	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4963	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2799	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2146  {cab 2744  ∃wrex 3092  ∪ ciun 4961

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 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rex 3093  df-iun 4963

This theorem is used by:  iunxdif2  5023  otiunsndisj  5508  onfununi  8337  oelim2  8590  marypha2lem2  9406  ttrclselem1  9704  ttrclselem2  9705  trcl  9707  r1om  10245  fictb  10246  cfsmolem  10272  cfsmo  10273  domtriomlem  10444  domtriom  10445  pwfseq  10667  wunex2  10741  wuncval2  10750  fsuppmapnn0fiubex  14048  s3iunsndisj  15031  ackbijnn  15908  smndex1basss  18992  smndex1mgm  18994  efgs1b  19831  ablfaclem3  20184  ptbasfi  23768  bcth3  25520  itg1climres  25903  suppovss  33056  hashunif  33181  gsumwrd2dccat  33422  fldextrspunlsplem  34087  bnj601  35332  cvmliftlem15  35803  neibastop2  36905  filnetlem4  36925  sstotbnd2  38458  heiborlem3  38497  heibor  38505  lcfr  42392  mapdrval  42454  corclrcl  44466  trclrelexplem  44470  dftrcl3  44479  cotrcltrcl  44484  dfrtrcl3  44492  corcltrcl  44498  cotrclrcl  44501  ssmapsn  45965  cnrefiisplem  46576  cnrefiisp  46577  meaiuninclem  47227  meaiuninc  47228  meaiininc  47234  carageniuncllem2  47269  caratheodorylem1  47273  caratheodorylem2  47274  caratheodory  47275  ovnsubadd  47319  hoidmv1le  47341  hoidmvle  47347  ovnhoilem2  47349  hspmbl  47376  ovnovollem3  47405  vonvolmbl  47408  smflimlem2  47519  smflimlem3  47520  smflimlem4  47521  smflim  47524  smflim2  47553  smflimsup  47575  otiunsndisjX  48049