Theorem cbviunv 4981

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 4983 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 3216	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2803	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4935	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4935	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2769	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {cab 2714  ∃wrex 3061  ∪ ciun 4933

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3062  df-iun 4935

This theorem is referenced by:  iunxdif2  4996  otiunsndisj  5474  onfununi  8281  oelim2  8531  marypha2lem2  9349  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  13954  s3iunsndisj  14930  ackbijnn  15793  smndex1basss  18876  smndex1mgm  18878  efgs1b  19711  ablfaclem3  20064  ptbasfi  23546  bcth3  25298  itg1climres  25681  suppovss  32754  hashunif  32879  gsumwrd2dccat  33139  fldextrspunlsplem  33817  bnj601  35062  cvmliftlem15  35480  neibastop2  36543  filnetlem4  36563  sstotbnd2  38095  heiborlem3  38134  heibor  38142  lcfr  42031  mapdrval  42093  corclrcl  44134  trclrelexplem  44138  dftrcl3  44147  cotrcltrcl  44152  dfrtrcl3  44160  corcltrcl  44166  cotrclrcl  44169  ssmapsn  45645  cnrefiisplem  46257  cnrefiisp  46258  meaiuninclem  46908  meaiuninc  46909  meaiininc  46915  carageniuncllem2  46950  caratheodorylem1  46954  caratheodorylem2  46955  caratheodory  46956  ovnsubadd  47000  hoidmv1le  47022  hoidmvle  47028  ovnhoilem2  47030  hspmbl  47057  ovnovollem3  47086  vonvolmbl  47089  smflimlem2  47200  smflimlem3  47201  smflimlem4  47202  smflim  47205  smflim2  47234  smflimsup  47256  otiunsndisjX  47727