MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cbviunv Unicode version

Theorem cbviunv 4064
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
StepHypRef Expression
1 nfcv 2516 . 2  |-  F/_ y B
2 nfcv 2516 . 2  |-  F/_ x C
3 cbviunv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbviun 4062 1  |-  U_ x  e.  A  B  =  U_ y  e.  A  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649   U_ciun 4028
This theorem is referenced by:  iunxdif2  4073  onfununi  6532  oelim2  6767  marypha2lem2  7369  trcl  7590  r1om  8050  fictb  8051  cfsmolem  8076  cfsmo  8077  domtriomlem  8248  domtriom  8249  pwfseq  8465  wunex2  8539  wuncval2  8548  ackbijnn  12527  efgs1b  15288  ablfaclem3  15565  ptbasfi  17527  bcth3  19146  itg1climres  19466  hashunif  23989  cvmliftlem15  24757  trpredlem1  25247  trpredtr  25250  trpredmintr  25251  trpredrec  25258  neibastop2  26074  filnetlem4  26094  sstotbnd2  26167  heiborlem3  26206  heibor  26214  bnj601  28622  lcfr  31751  mapdrval  31813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ral 2647  df-rex 2648  df-iun 4030
  Copyright terms: Public domain W3C validator