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 2402. 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 2847	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3242	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2828	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4953	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4953	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2794	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {cab 2739  ∃wrex 3087  ∪ 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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rex 3088  df-iun 4953

This theorem is used by:  iunxdif2  5012  otiunsndisj  5493  onfununi  8342  oelim2  8597  marypha2lem2  9421  ttrclselem1  9719  ttrclselem2  9720  trcl  9722  hfom  10314  fictb  10315  cfsmolem  10341  cfsmo  10342  domtriomlem  10513  domtriom  10514  pwfseq  10742  wunex2  10816  wuncval2  10825  fsuppmapnn0fiubex  14128  s3iunsndisj  15114  ackbijnn  15990  smndex1basss  19097  smndex1mgm  19099  efgs1b  19943  ablfaclem3  20296  ptbasfi  23893  bcth3  25645  itg1climres  26028  suppovss  33267  hashunif  33391  gsumwrd2dccat  33632  fldextrspunlsplem  34298  bnj601  35543  cvmliftlem15  36042  neibastop2  37129  filnetlem4  37149  sstotbnd2  38688  heiborlem3  38727  heibor  38735  lcfr  42622  mapdrval  42684  corclrcl  44692  trclrelexplem  44696  dftrcl3  44705  cotrcltrcl  44710  dfrtrcl3  44718  corcltrcl  44724  cotrclrcl  44727  ssmapsn  46198  cnrefiisplem  46808  cnrefiisp  46809  meaiuninclem  47459  meaiuninc  47460  meaiininc  47466  carageniuncllem2  47501  caratheodorylem1  47505  caratheodorylem2  47506  caratheodory  47507  ovnsubadd  47551  hoidmv1le  47573  hoidmvle  47579  ovnhoilem2  47581  hspmbl  47608  ovnovollem3  47637  vonvolmbl  47640  smflimlem2  47751  smflimlem3  47752  smflimlem4  47753  smflim  47756  smflim2  47785  smflimsup  47807  otiunsndisjX  48318