Theorem cbviunv 4958

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 2386. See cbviunvg 4960 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)

Hypothesis

Ref	Expression
cbviunv.1	⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)

Assertion

Ref	Expression
cbviunv	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbviunv

Step	Hyp	Ref	Expression
1		nfcv 2977	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2977	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 4954	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1533  ∪ ciun 4912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-iun 4914

This theorem is referenced by:  iunxdif2  4970  otiunsndisj  5403  onfununi  7972  oelim2  8215  marypha2lem2  8894  trcl  9164  r1om  9660  fictb  9661  cfsmolem  9686  cfsmo  9687  domtriomlem  9858  domtriom  9859  pwfseq  10080  wunex2  10154  wuncval2  10163  fsuppmapnn0fiubex  13354  s3iunsndisj  14322  ackbijnn  15177  smndex1basss  18064  smndex1mgm  18066  efgs1b  18856  ablfaclem3  19203  ptbasfi  22183  bcth3  23928  itg1climres  24309  suppovss  30420  hashunif  30522  bnj601  32187  cvmliftlem15  32540  trpredlem1  33061  trpredtr  33064  trpredmintr  33065  trpredrec  33072  neibastop2  33704  filnetlem4  33724  sstotbnd2  35046  heiborlem3  35085  heibor  35093  lcfr  38715  mapdrval  38777  corclrcl  40045  trclrelexplem  40049  dftrcl3  40058  cotrcltrcl  40063  dfrtrcl3  40071  corcltrcl  40077  cotrclrcl  40080  ssmapsn  41471  cnrefiisplem  42102  cnrefiisp  42103  meaiuninclem  42755  meaiuninc  42756  meaiininc  42762  carageniuncllem2  42797  caratheodorylem1  42801  caratheodorylem2  42802  caratheodory  42803  ovnsubadd  42847  hoidmv1le  42869  hoidmvle  42875  ovnhoilem2  42877  hspmbl  42904  ovnovollem3  42933  vonvolmbl  42936  smflimlem2  43041  smflimlem3  43042  smflimlem4  43043  smflim  43046  smflim2  43073  smflimsup  43095  otiunsndisjX  43471