Theorem cbviunv 4992

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 2374. See cbviunvg 4994 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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3213	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2801	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4946	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4946	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2767	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {cab 2712  ∃wrex 3058  ∪ ciun 4944

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rex 3059  df-iun 4946

This theorem is referenced by:  iunxdif2  5007  otiunsndisj  5466  onfununi  8271  oelim2  8521  marypha2lem2  9337  ttrclselem1  9632  ttrclselem2  9633  trcl  9635  r1om  10151  fictb  10152  cfsmolem  10178  cfsmo  10179  domtriomlem  10350  domtriom  10351  pwfseq  10573  wunex2  10647  wuncval2  10656  fsuppmapnn0fiubex  13913  s3iunsndisj  14889  ackbijnn  15749  smndex1basss  18828  smndex1mgm  18830  efgs1b  19663  ablfaclem3  20016  ptbasfi  23523  bcth3  25285  itg1climres  25669  suppovss  32709  hashunif  32835  gsumwrd2dccat  33109  fldextrspunlsplem  33779  bnj601  35025  cvmliftlem15  35441  neibastop2  36504  filnetlem4  36524  sstotbnd2  37914  heiborlem3  37953  heibor  37961  lcfr  41784  mapdrval  41846  corclrcl  43890  trclrelexplem  43894  dftrcl3  43903  cotrcltrcl  43908  dfrtrcl3  43916  corcltrcl  43922  cotrclrcl  43925  ssmapsn  45402  cnrefiisplem  46015  cnrefiisp  46016  meaiuninclem  46666  meaiuninc  46667  meaiininc  46673  carageniuncllem2  46708  caratheodorylem1  46712  caratheodorylem2  46713  caratheodory  46714  ovnsubadd  46758  hoidmv1le  46780  hoidmvle  46786  ovnhoilem2  46788  hspmbl  46815  ovnovollem3  46844  vonvolmbl  46847  smflimlem2  46958  smflimlem3  46959  smflimlem4  46960  smflim  46963  smflim2  46992  smflimsup  47014  otiunsndisjX  47467