Theorem cbviunv 4495

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.)

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 2751	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2751	. 2 ⊢ Ⅎ𝑥𝐶
3		cbviunv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbviun 4493	1 ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ 𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1475  ∪ ciun 4455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-iun 4457

This theorem is referenced by:  iunxdif2  4504  otiunsndisj  4905  onfununi  7325  oelim2  7562  marypha2lem2  8225  trcl  8487  r1om  8949  fictb  8950  cfsmolem  8975  cfsmo  8976  domtriomlem  9147  domtriom  9148  pwfseq  9365  wunex2  9439  wuncval2  9448  fsuppmapnn0fiubex  12654  s3iunsndisj  13555  ackbijnn  14399  efgs1b  17972  ablfaclem3  18309  ptbasfi  21194  bcth3  22936  itg1climres  23287  2spotiundisj  26589  hashunif  28949  bnj601  30244  cvmliftlem15  30534  trpredlem1  30971  trpredtr  30974  trpredmintr  30975  trpredrec  30982  neibastop2  31526  filnetlem4  31546  sstotbnd2  32743  heiborlem3  32782  heibor  32790  lcfr  35892  mapdrval  35954  corclrcl  37018  trclrelexplem  37022  dftrcl3  37031  cotrcltrcl  37036  dfrtrcl3  37044  corcltrcl  37050  cotrclrcl  37053  ssmapsn  38403  meaiuninclem  39373  meaiuninc  39374  meaiininc  39377  carageniuncllem2  39412  caratheodorylem1  39416  caratheodorylem2  39417  caratheodory  39418  ovnsubadd  39462  hoidmv1le  39484  hoidmvle  39490  ovnhoilem2  39492  hspmbl  39519  ovnovollem3  39548  vonvolmbl  39551  smflimlem2  39658  smflimlem3  39659  smflimlem4  39660  smflim  39663  otiunsndisjX  40317  2wspiundisj  41166