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

Theorem cbviunv 4550
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 2762 . 2 𝑦𝐵
2 nfcv 2762 . 2 𝑥𝐶
3 cbviunv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbviun 4548 1 𝑥𝐴 𝐵 = 𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481   ciun 4511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ral 2914  df-rex 2915  df-iun 4513
This theorem is referenced by:  iunxdif2  4559  otiunsndisj  4970  onfununi  7423  oelim2  7660  marypha2lem2  8327  trcl  8589  r1om  9051  fictb  9052  cfsmolem  9077  cfsmo  9078  domtriomlem  9249  domtriom  9250  pwfseq  9471  wunex2  9545  wuncval2  9554  fsuppmapnn0fiubex  12775  s3iunsndisj  13688  ackbijnn  14541  efgs1b  18130  ablfaclem3  18467  ptbasfi  21365  bcth3  23109  itg1climres  23462  hashunif  29536  bnj601  30964  cvmliftlem15  31254  trpredlem1  31701  trpredtr  31704  trpredmintr  31705  trpredrec  31712  neibastop2  32331  filnetlem4  32351  sstotbnd2  33544  heiborlem3  33583  heibor  33591  lcfr  36693  mapdrval  36755  corclrcl  37818  trclrelexplem  37822  dftrcl3  37831  cotrcltrcl  37836  dfrtrcl3  37844  corcltrcl  37850  cotrclrcl  37853  ssmapsn  39224  meaiuninclem  40460  meaiuninc  40461  meaiininc  40464  carageniuncllem2  40499  caratheodorylem1  40503  caratheodorylem2  40504  caratheodory  40505  ovnsubadd  40549  hoidmv1le  40571  hoidmvle  40577  ovnhoilem2  40579  hspmbl  40606  ovnovollem3  40635  vonvolmbl  40638  smflimlem2  40743  smflimlem3  40744  smflimlem4  40745  smflim  40748  smflim2  40775  smflimsup  40797  otiunsndisjX  41061
  Copyright terms: Public domain W3C validator