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

Theorem cbviunv 4667
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 2866 . 2 𝑦𝐵
2 nfcv 2866 . 2 𝑥𝐶
3 cbviunv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbviun 4665 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596   ciun 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-iun 4630
This theorem is referenced by:  iunxdif2  4676  otiunsndisj  5084  onfununi  7558  oelim2  7795  marypha2lem2  8458  trcl  8717  r1om  9179  fictb  9180  cfsmolem  9205  cfsmo  9206  domtriomlem  9377  domtriom  9378  pwfseq  9599  wunex2  9673  wuncval2  9682  fsuppmapnn0fiubex  12907  s3iunsndisj  13829  ackbijnn  14680  efgs1b  18270  ablfaclem3  18607  ptbasfi  21507  bcth3  23249  itg1climres  23601  hashunif  29792  bnj601  31218  cvmliftlem15  31508  trpredlem1  31953  trpredtr  31956  trpredmintr  31957  trpredrec  31964  neibastop2  32583  filnetlem4  32603  sstotbnd2  33805  heiborlem3  33844  heibor  33852  lcfr  37293  mapdrval  37355  corclrcl  38418  trclrelexplem  38422  dftrcl3  38431  cotrcltrcl  38436  dfrtrcl3  38444  corcltrcl  38450  cotrclrcl  38453  ssmapsn  39824  cnrefiisplem  40475  cnrefiisp  40476  meaiuninclem  41117  meaiuninc  41118  meaiininc  41124  carageniuncllem2  41159  caratheodorylem1  41163  caratheodorylem2  41164  caratheodory  41165  ovnsubadd  41209  hoidmv1le  41231  hoidmvle  41237  ovnhoilem2  41239  hspmbl  41266  ovnovollem3  41295  vonvolmbl  41298  smflimlem2  41403  smflimlem3  41404  smflimlem4  41405  smflim  41408  smflim2  41435  smflimsup  41457  otiunsndisjX  41723
  Copyright terms: Public domain W3C validator