Theorem cbviunv 4996

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 2377. See cbviunvg 4998 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 2823	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3217	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2804	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4950	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4950	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2770	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2715  ∃wrex 3062  ∪ ciun 4948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rex 3063  df-iun 4950

This theorem is referenced by:  iunxdif2  5011  otiunsndisj  5476  onfununi  8283  oelim2  8533  marypha2lem2  9351  ttrclselem1  9646  ttrclselem2  9647  trcl  9649  r1om  10165  fictb  10166  cfsmolem  10192  cfsmo  10193  domtriomlem  10364  domtriom  10365  pwfseq  10587  wunex2  10661  wuncval2  10670  fsuppmapnn0fiubex  13927  s3iunsndisj  14903  ackbijnn  15763  smndex1basss  18842  smndex1mgm  18844  efgs1b  19677  ablfaclem3  20030  ptbasfi  23537  bcth3  25299  itg1climres  25683  suppovss  32771  hashunif  32897  gsumwrd2dccat  33172  fldextrspunlsplem  33851  bnj601  35096  cvmliftlem15  35514  neibastop2  36577  filnetlem4  36597  sstotbnd2  38025  heiborlem3  38064  heibor  38072  lcfr  41961  mapdrval  42023  corclrcl  44063  trclrelexplem  44067  dftrcl3  44076  cotrcltrcl  44081  dfrtrcl3  44089  corcltrcl  44095  cotrclrcl  44098  ssmapsn  45574  cnrefiisplem  46187  cnrefiisp  46188  meaiuninclem  46838  meaiuninc  46839  meaiininc  46845  carageniuncllem2  46880  caratheodorylem1  46884  caratheodorylem2  46885  caratheodory  46886  ovnsubadd  46930  hoidmv1le  46952  hoidmvle  46958  ovnhoilem2  46960  hspmbl  46987  ovnovollem3  47016  vonvolmbl  47019  smflimlem2  47130  smflimlem3  47131  smflimlem4  47132  smflim  47135  smflim2  47164  smflimsup  47186  otiunsndisjX  47639