Theorem cbviunv 5003

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 2404. See cbviunvg 5005 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 2849	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 ∈ 𝐵 ↔ 𝑧 ∈ 𝐶))
3	2	cbvrexvw 3244	. . 3 ⊢ (∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 ↔ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶)
4	3	abbii 2830	. 2 ⊢ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵} = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
5		df-iun 4958	. 2 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 ∈ 𝐵}
6		df-iun 4958	. 2 ⊢ ∪ 𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ ∃𝑦 ∈ 𝐴 𝑧 ∈ 𝐶}
7	4, 5, 6	3eqtr4i 2796	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {cab 2741  ∃wrex 3089  ∪ ciun 4956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rex 3090  df-iun 4958

This theorem is referenced by:  iunxdif2  5018  otiunsndisj  5503  onfununi  8324  oelim2  8577  marypha2lem2  9392  ttrclselem1  9690  ttrclselem2  9691  trcl  9693  r1om  10222  fictb  10223  cfsmolem  10249  cfsmo  10250  domtriomlem  10421  domtriom  10422  pwfseq  10644  wunex2  10718  wuncval2  10727  fsuppmapnn0fiubex  14024  s3iunsndisj  15001  ackbijnn  15878  smndex1basss  18962  smndex1mgm  18964  efgs1b  19801  ablfaclem3  20154  ptbasfi  23738  bcth3  25490  itg1climres  25873  suppovss  33026  hashunif  33151  gsumwrd2dccat  33398  fldextrspunlsplem  34063  bnj601  35308  cvmliftlem15  35790  neibastop2  36872  filnetlem4  36892  sstotbnd2  38425  heiborlem3  38464  heibor  38472  lcfr  42359  mapdrval  42421  corclrcl  44433  trclrelexplem  44437  dftrcl3  44446  cotrcltrcl  44451  dfrtrcl3  44459  corcltrcl  44465  cotrclrcl  44468  ssmapsn  45932  cnrefiisplem  46543  cnrefiisp  46544  meaiuninclem  47194  meaiuninc  47195  meaiininc  47201  carageniuncllem2  47236  caratheodorylem1  47240  caratheodorylem2  47241  caratheodory  47242  ovnsubadd  47286  hoidmv1le  47308  hoidmvle  47314  ovnhoilem2  47316  hspmbl  47343  ovnovollem3  47372  vonvolmbl  47375  smflimlem2  47486  smflimlem3  47487  smflimlem4  47488  smflim  47491  smflim2  47520  smflimsup  47542  otiunsndisjX  48016