Theorem cbviunv 4341

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 2591	. 2 |- F/_ y B
2		nfcv 2591	. 2 |- F/_ x C
3		cbviunv.1	. 2 |- ( x = y -> B = C )
4	1, 2, 3	cbviun 4339	1 |- U_ x e. A B = U_ y e. A C

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-rex 2788  df-iun 4304

This theorem is referenced by:  iunxdif2  4350  otiunsndisj  4727  onfununi  7068  oelim2  7304  marypha2lem2  7956  trcl  8211  r1om  8672  fictb  8673  cfsmolem  8698  cfsmo  8699  domtriomlem  8870  domtriom  8871  pwfseq  9088  wunex2  9162  wuncval2  9171  fsuppmapnn0fiubex  12201  ackbijnn  13864  efgs1b  17321  ablfaclem3  17655  ptbasfi  20527  bcth3  22192  itg1climres  22549  2spotiundisj  25635  hashunif  28216  bnj601  29519  cvmliftlem15  29809  trpredlem1  30255  trpredtr  30258  trpredmintr  30259  trpredrec  30266  neibastop2  30802  filnetlem4  30822  sstotbnd2  31810  heiborlem3  31849  heibor  31857  lcfr  34862  mapdrval  34924  corclrcl  35938  trclrelexplem  35942  dftrcl3  35951  cotrcltrcl  35956  dfrtrcl3  35964  corcltrcl  35970  cotrclrcl  35973  carageniuncllem2  37852  caratheodorylem1  37856  caratheodorylem2  37857  caratheodory  37858  otiunsndisjX  38378