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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ∈ wcel 2144  {cab 2738  ∃wrex 3086  ∪ ciun 4950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rex 3087  df-iun 4952

This theorem is used by:  iunxdif2  5011  otiunsndisj  5493  onfununi  8356  oelim2  8611  marypha2lem2  9435  ttrclselem1  9733  ttrclselem2  9734  trcl  9736  hfom  10328  fictb  10329  cfsmolem  10355  cfsmo  10356  domtriomlem  10527  domtriom  10528  pwfseq  10756  wunex2  10830  wuncval2  10839  fsuppmapnn0fiubex  14142  s3iunsndisj  15130  ackbijnn  16006  smndex1basss  19113  smndex1mgm  19115  efgs1b  19959  ablfaclem3  20312  ptbasfi  23909  bcth3  25661  itg1climres  26044  suppovss  33325  hashunif  33448  gsumwrd2dccat  33689  fldextrspunlsplem  34355  bnj601  35600  cvmliftlem15  36153  neibastop2  37245  filnetlem4  37265  sstotbnd2  38817  heiborlem3  38856  heibor  38864  lcfr  42751  mapdrval  42813  corclrcl  44816  trclrelexplem  44820  dftrcl3  44829  cotrcltrcl  44834  dfrtrcl3  44842  corcltrcl  44848  cotrclrcl  44851  ssmapsn  46337  cnrefiisplem  46947  cnrefiisp  46948  meaiuninclem  47598  meaiuninc  47599  meaiininc  47605  carageniuncllem2  47640  caratheodorylem1  47644  caratheodorylem2  47645  caratheodory  47646  ovnsubadd  47690  hoidmv1le  47712  hoidmvle  47718  ovnhoilem2  47720  hspmbl  47747  ovnovollem3  47776  vonvolmbl  47779  smflimlem2  47890  smflimlem3  47891  smflimlem4  47892  smflim  47895  smflim2  47924  smflimsup  47946  otiunsndisjX  48457