Theorem cbvixpv 8911

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

Syntax hints:   → wi 4   = wceq 1539  Xcixp 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-iota 6494  df-fn 6545  df-fv 6550  df-ixp 8894

This theorem is referenced by:  funcpropd  17855  invfuc  17931  natpropd  17933  dprdw  19921  dprdwd  19922  ptuni2  23300  ptbasin  23301  ptbasfi  23305  ptpjopn  23336  ptclsg  23339  dfac14  23342  ptcnp  23346  ptcmplem2  23777  ptcmpg  23781  prdsxmslem2  24258  upixp  36900  rrxsnicc  45314  ioorrnopn  45319  ioorrnopnxr  45321  ovnsubadd  45586  hoidmvlelem4  45612  hoidmvle  45614  hspdifhsp  45630  hoiqssbllem2  45637  hspmbl  45643  hoimbl  45645  opnvonmbl  45648  ovnovollem3  45672