Theorem cbviunv 4221

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

Syntax hints:   -> wi 4   = wceq 1369   U_ciun 4183

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ral 2732  df-rex 2733  df-iun 4185

This theorem is referenced by:  iunxdif2  4230  onfununi  6814  oelim2  7046  marypha2lem2  7698  trcl  7960  r1om  8425  fictb  8426  cfsmolem  8451  cfsmo  8452  domtriomlem  8623  domtriom  8624  pwfseq  8843  wunex2  8917  wuncval2  8926  ackbijnn  13303  efgs1b  16245  ablfaclem3  16600  ptbasfi  19166  bcth3  20854  itg1climres  21204  hashunif  26096  cvmliftlem15  27199  trpredlem1  27703  trpredtr  27706  trpredmintr  27707  trpredrec  27714  neibastop2  28594  filnetlem4  28614  sstotbnd2  28685  heiborlem3  28724  heibor  28732  otiunsndisj  30144  otiunsndisjX  30145  2spotiundisj  30667  fsuppmapnn0fiubex  30812  bnj601  31925  lcfr  35242  mapdrval  35304