Theorem cbviunv 4989

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 2370. See cbviunvg 4991 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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3208	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2796	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4943	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4943	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {cab 2707  ∃wrex 3053  ∪ ciun 4941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rex 3054  df-iun 4943

This theorem is referenced by:  iunxdif2  5002  otiunsndisj  5463  onfununi  8264  oelim2  8513  marypha2lem2  9326  ttrclselem1  9621  ttrclselem2  9622  trcl  9624  r1om  10137  fictb  10138  cfsmolem  10164  cfsmo  10165  domtriomlem  10336  domtriom  10337  pwfseq  10558  wunex2  10632  wuncval2  10641  fsuppmapnn0fiubex  13899  s3iunsndisj  14875  ackbijnn  15735  smndex1basss  18779  smndex1mgm  18781  efgs1b  19615  ablfaclem3  19968  ptbasfi  23466  bcth3  25229  itg1climres  25613  suppovss  32623  hashunif  32751  gsumwrd2dccat  33020  fldextrspunlsplem  33640  bnj601  34887  cvmliftlem15  35271  neibastop2  36335  filnetlem4  36355  sstotbnd2  37754  heiborlem3  37793  heibor  37801  lcfr  41564  mapdrval  41626  corclrcl  43680  trclrelexplem  43684  dftrcl3  43693  cotrcltrcl  43698  dfrtrcl3  43706  corcltrcl  43712  cotrclrcl  43715  ssmapsn  45194  cnrefiisplem  45810  cnrefiisp  45811  meaiuninclem  46461  meaiuninc  46462  meaiininc  46468  carageniuncllem2  46503  caratheodorylem1  46507  caratheodorylem2  46508  caratheodory  46509  ovnsubadd  46553  hoidmv1le  46575  hoidmvle  46581  ovnhoilem2  46583  hspmbl  46610  ovnovollem3  46639  vonvolmbl  46642  smflimlem2  46753  smflimlem3  46754  smflimlem4  46755  smflim  46758  smflim2  46787  smflimsup  46809  otiunsndisjX  47263