Theorem cbviunv 4997

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 2401. See cbviunvg 4999 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 2846	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3241	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2827	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4953	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4953	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2793	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2738  ∃wrex 3086  ∪ ciun 4951

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 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-iun 4953

This theorem is used by:  iunxdif2  5012  otiunsndisj  5497  onfununi  8330  oelim2  8583  marypha2lem2  9406  ttrclselem1  9704  ttrclselem2  9705  trcl  9707  r1om  10245  fictb  10246  cfsmolem  10272  cfsmo  10273  domtriomlem  10444  domtriom  10445  pwfseq  10673  wunex2  10747  wuncval2  10756  fsuppmapnn0fiubex  14056  s3iunsndisj  15041  ackbijnn  15917  smndex1basss  19017  smndex1mgm  19019  efgs1b  19863  ablfaclem3  20216  ptbasfi  23807  bcth3  25559  itg1climres  25942  suppovss  33153  hashunif  33277  gsumwrd2dccat  33518  fldextrspunlsplem  34183  bnj601  35429  cvmliftlem15  35877  neibastop2  36980  filnetlem4  37000  sstotbnd2  38524  heiborlem3  38563  heibor  38571  lcfr  42458  mapdrval  42520  corclrcl  44547  trclrelexplem  44551  dftrcl3  44560  cotrcltrcl  44565  dfrtrcl3  44573  corcltrcl  44579  cotrclrcl  44582  ssmapsn  46046  cnrefiisplem  46657  cnrefiisp  46658  meaiuninclem  47308  meaiuninc  47309  meaiininc  47315  carageniuncllem2  47350  caratheodorylem1  47354  caratheodorylem2  47355  caratheodory  47356  ovnsubadd  47400  hoidmv1le  47422  hoidmvle  47428  ovnhoilem2  47430  hspmbl  47457  ovnovollem3  47486  vonvolmbl  47489  smflimlem2  47600  smflimlem3  47601  smflimlem4  47602  smflim  47605  smflim2  47634  smflimsup  47656  otiunsndisjX  48167