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

Theorem cbvixpv 7871
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 2767 . 2 𝑦𝐵
2 nfcv 2767 . 2 𝑥𝐶
3 cbvixpv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvixp 7870 1 X𝑥𝐴 𝐵 = X𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  Xcixp 7853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fn 5853  df-fv 5858  df-ixp 7854
This theorem is referenced by:  funcpropd  16476  invfuc  16550  natpropd  16552  dprdw  18325  dprdwd  18326  ptuni2  21284  ptbasin  21285  ptbasfi  21289  ptpjopn  21320  ptclsg  21323  dfac14  21326  ptcnp  21330  ptcmplem2  21762  ptcmpg  21766  prdsxmslem2  22239  upixp  33142  rrxsnicc  39814  ioorrnopn  39819  ioorrnopnxr  39821  ovnsubadd  40080  hoidmvlelem4  40106  hoidmvle  40108  hspdifhsp  40124  hoiqssbllem2  40131  hspmbl  40137  hoimbl  40139  opnvonmbl  40142  ovnovollem3  40166
  Copyright terms: Public domain W3C validator