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

Theorem cbvixpv 8856
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 2904 . 2 𝑦𝐵
2 nfcv 2904 . 2 𝑥𝐶
3 cbvixpv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvixp 8855 1 X𝑥𝐴 𝐵 = X𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  Xcixp 8838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ral 3062  df-rab 3407  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-iota 6449  df-fn 6500  df-fv 6505  df-ixp 8839
This theorem is referenced by:  funcpropd  17792  invfuc  17868  natpropd  17870  dprdw  19794  dprdwd  19795  ptuni2  22943  ptbasin  22944  ptbasfi  22948  ptpjopn  22979  ptclsg  22982  dfac14  22985  ptcnp  22989  ptcmplem2  23420  ptcmpg  23424  prdsxmslem2  23901  upixp  36234  rrxsnicc  44627  ioorrnopn  44632  ioorrnopnxr  44634  ovnsubadd  44899  hoidmvlelem4  44925  hoidmvle  44927  hspdifhsp  44943  hoiqssbllem2  44950  hspmbl  44956  hoimbl  44958  opnvonmbl  44961  ovnovollem3  44985
  Copyright terms: Public domain W3C validator