Theorem cbviunv 4331

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

Syntax hints:   -> wi 4   = wceq 1455   U_ciun 4292

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ral 2754  df-rex 2755  df-iun 4294

This theorem is referenced by:  iunxdif2  4340  otiunsndisj  4721  onfununi  7086  oelim2  7322  marypha2lem2  7976  trcl  8238  r1om  8700  fictb  8701  cfsmolem  8726  cfsmo  8727  domtriomlem  8898  domtriom  8899  pwfseq  9115  wunex2  9189  wuncval2  9198  fsuppmapnn0fiubex  12236  ackbijnn  13935  efgs1b  17435  ablfaclem3  17769  ptbasfi  20645  bcth3  22348  itg1climres  22721  2spotiundisj  25839  hashunif  28428  bnj601  29780  cvmliftlem15  30070  trpredlem1  30517  trpredtr  30520  trpredmintr  30521  trpredrec  30528  neibastop2  31066  filnetlem4  31086  sstotbnd2  32151  heiborlem3  32190  heibor  32198  lcfr  35198  mapdrval  35260  corclrcl  36344  trclrelexplem  36348  dftrcl3  36357  cotrcltrcl  36362  dfrtrcl3  36370  corcltrcl  36376  cotrclrcl  36379  carageniuncllem2  38381  caratheodorylem1  38385  caratheodorylem2  38386  caratheodory  38387  ovnsubadd  38432  hoidmv1le  38454  hoidmvle  38460  ovnhoilem2  38462  hspmbl  38489  otiunsndisjX  39046