Theorem cbviunv 4994

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {cab 2714  ∃wrex 3060  ∪ ciun 4946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rex 3061  df-iun 4948

This theorem is referenced by:  iunxdif2  5009  otiunsndisj  5468  onfununi  8273  oelim2  8523  marypha2lem2  9339  ttrclselem1  9634  ttrclselem2  9635  trcl  9637  r1om  10153  fictb  10154  cfsmolem  10180  cfsmo  10181  domtriomlem  10352  domtriom  10353  pwfseq  10575  wunex2  10649  wuncval2  10658  fsuppmapnn0fiubex  13915  s3iunsndisj  14891  ackbijnn  15751  smndex1basss  18830  smndex1mgm  18832  efgs1b  19665  ablfaclem3  20018  ptbasfi  23525  bcth3  25287  itg1climres  25671  suppovss  32760  hashunif  32886  gsumwrd2dccat  33160  fldextrspunlsplem  33830  bnj601  35076  cvmliftlem15  35492  neibastop2  36555  filnetlem4  36575  sstotbnd2  37971  heiborlem3  38010  heibor  38018  lcfr  41841  mapdrval  41903  corclrcl  43944  trclrelexplem  43948  dftrcl3  43957  cotrcltrcl  43962  dfrtrcl3  43970  corcltrcl  43976  cotrclrcl  43979  ssmapsn  45456  cnrefiisplem  46069  cnrefiisp  46070  meaiuninclem  46720  meaiuninc  46721  meaiininc  46727  carageniuncllem2  46762  caratheodorylem1  46766  caratheodorylem2  46767  caratheodory  46768  ovnsubadd  46812  hoidmv1le  46834  hoidmvle  46840  ovnhoilem2  46842  hspmbl  46869  ovnovollem3  46898  vonvolmbl  46901  smflimlem2  47012  smflimlem3  47013  smflimlem4  47014  smflim  47017  smflim2  47046  smflimsup  47068  otiunsndisjX  47521