Theorem cbvixpv 8462

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 2955	. 2 ⊢ Ⅎ𝑦𝐵
2		nfcv 2955	. 2 ⊢ Ⅎ𝑥𝐶
3		cbvixpv.1	. 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
4	1, 2, 3	cbvixp 8461	1 ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   = wceq 1538  Xcixp 8444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fn 6327  df-fv 6332  df-ixp 8445

This theorem is referenced by:  funcpropd  17162  invfuc  17236  natpropd  17238  dprdw  19125  dprdwd  19126  ptuni2  22181  ptbasin  22182  ptbasfi  22186  ptpjopn  22217  ptclsg  22220  dfac14  22223  ptcnp  22227  ptcmplem2  22658  ptcmpg  22662  prdsxmslem2  23136  upixp  35167  rrxsnicc  42942  ioorrnopn  42947  ioorrnopnxr  42949  ovnsubadd  43211  hoidmvlelem4  43237  hoidmvle  43239  hspdifhsp  43255  hoiqssbllem2  43262  hspmbl  43268  hoimbl  43270  opnvonmbl  43273  ovnovollem3  43297