Theorem cbvixpv 7968

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

Step	Hyp	Ref	Expression
1		nfcv 2793	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2793	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvixpv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvixp 7967	1 ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1523  Xcixp 7950

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fn 5929  df-fv 5934  df-ixp 7951

This theorem is referenced by:  funcpropd  16607  invfuc  16681  natpropd  16683  dprdw  18455  dprdwd  18456  ptuni2  21427  ptbasin  21428  ptbasfi  21432  ptpjopn  21463  ptclsg  21466  dfac14  21469  ptcnp  21473  ptcmplem2  21904  ptcmpg  21908  prdsxmslem2  22381  upixp  33654  rrxsnicc  40838  ioorrnopn  40843  ioorrnopnxr  40845  ovnsubadd  41107  hoidmvlelem4  41133  hoidmvle  41135  hspdifhsp  41151  hoiqssbllem2  41158  hspmbl  41164  hoimbl  41166  opnvonmbl  41169  ovnovollem3  41193