Theorem cbviunv 4794

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

Syntax hints:   → wi 4   = wceq 1601  ∪ ciun 4755

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-iun 4757

This theorem is referenced by:  iunxdif2  4803  otiunsndisj  5219  onfununi  7723  oelim2  7961  marypha2lem2  8632  trcl  8903  r1om  9403  fictb  9404  cfsmolem  9429  cfsmo  9430  domtriomlem  9601  domtriom  9602  pwfseq  9823  wunex2  9897  wuncval2  9906  fsuppmapnn0fiubex  13114  s3iunsndisj  14120  ackbijnn  14968  efgs1b  18537  ablfaclem3  18877  ptbasfi  21797  bcth3  23541  itg1climres  23922  hashunif  30130  bnj601  31593  cvmliftlem15  31883  trpredlem1  32319  trpredtr  32322  trpredmintr  32323  trpredrec  32330  neibastop2  32948  filnetlem4  32968  sstotbnd2  34202  heiborlem3  34241  heibor  34249  lcfr  37744  mapdrval  37806  corclrcl  38966  trclrelexplem  38970  dftrcl3  38979  cotrcltrcl  38984  dfrtrcl3  38992  corcltrcl  38998  cotrclrcl  39001  ssmapsn  40339  cnrefiisplem  40979  cnrefiisp  40980  meaiuninclem  41631  meaiuninc  41632  meaiininc  41638  carageniuncllem2  41673  caratheodorylem1  41677  caratheodorylem2  41678  caratheodory  41679  ovnsubadd  41723  hoidmv1le  41745  hoidmvle  41751  ovnhoilem2  41753  hspmbl  41780  ovnovollem3  41809  vonvolmbl  41812  smflimlem2  41917  smflimlem3  41918  smflimlem4  41919  smflim  41922  smflim2  41949  smflimsup  41971  otiunsndisjX  42330