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 2403. 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 2848	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3241	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2829	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4951	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4951	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2795	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1560   ∈ wcel 2142  {cab 2740  ∃wrex 3086  ∪ ciun 4949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rex 3087  df-iun 4951

This theorem is referenced by:  iunxdif2  5011  otiunsndisj  5489  onfununi  8312  oelim2  8565  marypha2lem2  9382  ttrclselem1  9680  ttrclselem2  9681  trcl  9683  r1om  10199  fictb  10200  cfsmolem  10227  cfsmo  10228  domtriomlem  10399  domtriom  10400  pwfseq  10622  wunex2  10696  wuncval2  10705  fsuppmapnn0fiubex  14005  s3iunsndisj  14981  ackbijnn  15858  smndex1basss  18942  smndex1mgm  18944  efgs1b  19776  ablfaclem3  20129  ptbasfi  23638  bcth3  25390  itg1climres  25773  suppovss  32880  hashunif  33005  gsumwrd2dccat  33255  fldextrspunlsplem  33967  bnj601  35212  cvmliftlem15  35645  neibastop2  36718  filnetlem4  36738  sstotbnd2  38270  heiborlem3  38309  heibor  38317  lcfr  42206  mapdrval  42268  corclrcl  44280  trclrelexplem  44284  dftrcl3  44293  cotrcltrcl  44298  dfrtrcl3  44306  corcltrcl  44312  cotrclrcl  44315  ssmapsn  45789  cnrefiisplem  46400  cnrefiisp  46401  meaiuninclem  47051  meaiuninc  47052  meaiininc  47058  carageniuncllem2  47093  caratheodorylem1  47097  caratheodorylem2  47098  caratheodory  47099  ovnsubadd  47143  hoidmv1le  47165  hoidmvle  47171  ovnhoilem2  47173  hspmbl  47200  ovnovollem3  47229  vonvolmbl  47232  smflimlem2  47343  smflimlem3  47344  smflimlem4  47345  smflim  47348  smflim2  47377  smflimsup  47399  otiunsndisjX  47870