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

Theorem cbviunv 4930
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.) Add disjoint variable condition to avoid ax-13 2382. See cbviunvg 4932 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024.)
Hypothesis
Ref Expression
cbviunv.1 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbviunv 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Distinct variable groups:   𝑥,𝑦,𝐴   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbviunv
StepHypRef Expression
1 nfcv 2958 . 2 𝑦𝐵
2 nfcv 2958 . 2 𝑥𝐶
3 cbviunv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbviun 4926 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538   ciun 4884
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-11 2159  ax-12 2176  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-iun 4886
This theorem is referenced by:  iunxdif2  4943  otiunsndisj  5378  onfununi  7965  oelim2  8208  marypha2lem2  8888  trcl  9158  r1om  9659  fictb  9660  cfsmolem  9685  cfsmo  9686  domtriomlem  9857  domtriom  9858  pwfseq  10079  wunex2  10153  wuncval2  10162  fsuppmapnn0fiubex  13359  s3iunsndisj  14323  ackbijnn  15178  smndex1basss  18065  smndex1mgm  18067  efgs1b  18857  ablfaclem3  19205  ptbasfi  22189  bcth3  23938  itg1climres  24321  suppovss  30446  hashunif  30557  bnj601  32300  cvmliftlem15  32653  trpredlem1  33174  trpredtr  33177  trpredmintr  33178  trpredrec  33185  neibastop2  33817  filnetlem4  33837  sstotbnd2  35205  heiborlem3  35244  heibor  35252  lcfr  38874  mapdrval  38936  corclrcl  40395  trclrelexplem  40399  dftrcl3  40408  cotrcltrcl  40413  dfrtrcl3  40421  corcltrcl  40427  cotrclrcl  40430  ssmapsn  41832  cnrefiisplem  42458  cnrefiisp  42459  meaiuninclem  43106  meaiuninc  43107  meaiininc  43113  carageniuncllem2  43148  caratheodorylem1  43152  caratheodorylem2  43153  caratheodory  43154  ovnsubadd  43198  hoidmv1le  43220  hoidmvle  43226  ovnhoilem2  43228  hspmbl  43255  ovnovollem3  43284  vonvolmbl  43287  smflimlem2  43392  smflimlem3  43393  smflimlem4  43394  smflim  43397  smflim2  43424  smflimsup  43446  otiunsndisjX  43822
  Copyright terms: Public domain W3C validator