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

Theorem cbviunv 4486
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 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbviunv 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Distinct variable groups:   𝑥,𝐴   𝑦,𝐴   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbviunv
StepHypRef Expression
1 nfcv 2747 . 2 𝑦𝐵
2 nfcv 2747 . 2 𝑥𝐶
3 cbviunv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbviun 4484 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474   ciun 4446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-iun 4448
This theorem is referenced by:  iunxdif2  4495  otiunsndisj  4893  onfununi  7299  oelim2  7536  marypha2lem2  8199  trcl  8461  r1om  8923  fictb  8924  cfsmolem  8949  cfsmo  8950  domtriomlem  9121  domtriom  9122  pwfseq  9339  wunex2  9413  wuncval2  9422  fsuppmapnn0fiubex  12606  s3iunsndisj  13498  ackbijnn  14342  efgs1b  17915  ablfaclem3  18252  ptbasfi  21133  bcth3  22850  itg1climres  23201  2spotiundisj  26352  hashunif  28752  bnj601  30047  cvmliftlem15  30337  trpredlem1  30774  trpredtr  30777  trpredmintr  30778  trpredrec  30785  neibastop2  31329  filnetlem4  31349  sstotbnd2  32543  heiborlem3  32582  heibor  32590  lcfr  35692  mapdrval  35754  corclrcl  36818  trclrelexplem  36822  dftrcl3  36831  cotrcltrcl  36836  dfrtrcl3  36844  corcltrcl  36850  cotrclrcl  36853  ssmapsn  38203  meaiuninclem  39174  meaiuninc  39175  meaiininc  39178  carageniuncllem2  39213  caratheodorylem1  39217  caratheodorylem2  39218  caratheodory  39219  ovnsubadd  39263  hoidmv1le  39285  hoidmvle  39291  ovnhoilem2  39293  hspmbl  39320  ovnovollem3  39349  vonvolmbl  39352  smflimlem2  39459  smflimlem3  39460  smflimlem4  39461  smflim  39464  otiunsndisjX  40129  2wspiundisj  41165
  Copyright terms: Public domain W3C validator