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

Theorem cbviunv 4122
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 2571 . 2  |-  F/_ y B
2 nfcv 2571 . 2  |-  F/_ x C
3 cbviunv.1 . 2  |-  ( x  =  y  ->  B  =  C )
41, 2, 3cbviun 4120 1  |-  U_ x  e.  A  B  =  U_ y  e.  A  C
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   U_ciun 4085
This theorem is referenced by:  iunxdif2  4131  onfununi  6595  oelim2  6830  marypha2lem2  7433  trcl  7656  r1om  8116  fictb  8117  cfsmolem  8142  cfsmo  8143  domtriomlem  8314  domtriom  8315  pwfseq  8531  wunex2  8605  wuncval2  8614  ackbijnn  12599  efgs1b  15360  ablfaclem3  15637  ptbasfi  17605  bcth3  19276  itg1climres  19598  hashunif  24150  cvmliftlem15  24977  trpredlem1  25497  trpredtr  25500  trpredmintr  25501  trpredrec  25508  neibastop2  26381  filnetlem4  26401  sstotbnd2  26474  heiborlem3  26513  heibor  26521  otiunsndisj  28056  otiunsndisjX  28057  2spotiundisj  28388  bnj601  29228  lcfr  32320  mapdrval  32382
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-iun 4087
  Copyright terms: Public domain W3C validator