Theorem cbviunv 4364

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

Syntax hints:   -> wi 4   = wceq 1379   U_ciun 4325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-iun 4327

This theorem is referenced by:  iunxdif2  4373  otiunsndisj  4753  onfununi  7013  oelim2  7245  marypha2lem2  7897  trcl  8160  r1om  8625  fictb  8626  cfsmolem  8651  cfsmo  8652  domtriomlem  8823  domtriom  8824  pwfseq  9043  wunex2  9117  wuncval2  9126  fsuppmapnn0fiubex  12067  ackbijnn  13606  efgs1b  16569  ablfaclem3  16952  ptbasfi  19909  bcth3  21597  itg1climres  21948  2spotiundisj  24836  hashunif  27370  cvmliftlem15  28494  trpredlem1  29163  trpredtr  29166  trpredmintr  29167  trpredrec  29174  neibastop2  30009  filnetlem4  30029  sstotbnd2  30100  heiborlem3  30139  heibor  30147  otiunsndisjX  31995  bnj601  33274  lcfr  36599  mapdrval  36661