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

Theorem cbvixpv 7812
Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009.)
Hypothesis
Ref Expression
cbvixpv.1 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvixpv X𝑥𝐴 𝐵 = X𝑦𝐴 𝐶
Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvixpv
StepHypRef Expression
1 nfcv 2751 . 2 𝑦𝐵
2 nfcv 2751 . 2 𝑥𝐶
3 cbvixpv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvixp 7811 1 X𝑥𝐴 𝐵 = X𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  Xcixp 7794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fn 5807  df-fv 5812  df-ixp 7795
This theorem is referenced by:  funcpropd  16383  invfuc  16457  natpropd  16459  dprdw  18232  dprdwd  18233  ptuni2  21189  ptbasin  21190  ptbasfi  21194  ptpjopn  21225  ptclsg  21228  dfac14  21231  ptcnp  21235  ptcmplem2  21667  ptcmpg  21671  prdsxmslem2  22144  upixp  32694  rrxsnicc  39196  ioorrnopn  39201  ioorrnopnxr  39203  ovnsubadd  39462  hoidmvlelem4  39488  hoidmvle  39490  hspdifhsp  39506  hoiqssbllem2  39513  hspmbl  39519  hoimbl  39521  opnvonmbl  39524  ovnovollem3  39548
  Copyright terms: Public domain W3C validator