Theorem cbviunv 4276

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	|- ( x = y -> B = C )

Assertion

Ref	Expression
cbviunv	|- U_ x e. A B = U_ y e. A C

Distinct variable groups:   x, A   y, A   y, B   x, C

Allowed substitution hints:   B( x)   C( y)

Proof of Theorem cbviunv

Step	Hyp	Ref	Expression
1		nfcv 2564	. 2 |- F/_ y B
2		nfcv 2564	. 2 |- F/_ x C
3		cbviunv.1	. 2 |- ( x = y -> B = C )
4	1, 2, 3	cbviun 4274	1 |- U_ x e. A B = U_ y e. A C

Syntax hints:   -> wi 4   = wceq 1437   U_ciun 4237

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ral 2714  df-rex 2715  df-iun 4239

This theorem is referenced by:  iunxdif2  4285  otiunsndisj  4664  onfununi  7010  oelim2  7246  marypha2lem2  7898  trcl  8159  r1om  8620  fictb  8621  cfsmolem  8646  cfsmo  8647  domtriomlem  8818  domtriom  8819  pwfseq  9035  wunex2  9109  wuncval2  9118  fsuppmapnn0fiubex  12149  ackbijnn  13824  efgs1b  17324  ablfaclem3  17658  ptbasfi  20533  bcth3  22236  itg1climres  22609  2spotiundisj  25727  hashunif  28325  bnj601  29678  cvmliftlem15  29968  trpredlem1  30414  trpredtr  30417  trpredmintr  30418  trpredrec  30425  neibastop2  30961  filnetlem4  30981  sstotbnd2  32013  heiborlem3  32052  heibor  32060  lcfr  35065  mapdrval  35127  corclrcl  36212  trclrelexplem  36216  dftrcl3  36225  cotrcltrcl  36230  dfrtrcl3  36238  corcltrcl  36244  cotrclrcl  36247  carageniuncllem2  38194  caratheodorylem1  38198  caratheodorylem2  38199  caratheodory  38200  ovnsubadd  38241  hoidmv1le  38263  hoidmvle  38269  ovnhoilem2  38271  otiunsndisjX  38814