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

Theorem cbvixpv 8457
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 2973 . 2 𝑦𝐵
2 nfcv 2973 . 2 𝑥𝐶
3 cbvixpv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvixp 8456 1 X𝑥𝐴 𝐵 = X𝑦𝐴 𝐶
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1537  Xcixp 8439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ral 3130  df-rab 3134  df-v 3475  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4270  df-if 4444  df-sn 4544  df-pr 4546  df-op 4550  df-uni 4815  df-br 5043  df-iota 6290  df-fn 6334  df-fv 6339  df-ixp 8440
This theorem is referenced by:  funcpropd  17149  invfuc  17223  natpropd  17225  dprdw  19111  dprdwd  19112  ptuni2  22160  ptbasin  22161  ptbasfi  22165  ptpjopn  22196  ptclsg  22199  dfac14  22202  ptcnp  22206  ptcmplem2  22637  ptcmpg  22641  prdsxmslem2  23115  upixp  35043  rrxsnicc  42733  ioorrnopn  42738  ioorrnopnxr  42740  ovnsubadd  43002  hoidmvlelem4  43028  hoidmvle  43030  hspdifhsp  43046  hoiqssbllem2  43053  hspmbl  43059  hoimbl  43061  opnvonmbl  43064  ovnovollem3  43088
  Copyright terms: Public domain W3C validator