Theorem cbvixpv 8914

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

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6883	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑧‘𝑥) = (𝑧‘𝑦))
2		cbvixpv.1	. . . . . 6 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	1, 2	eleq12d 2857	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑧‘𝑥) ∈ 𝐵 ↔ (𝑧‘𝑦) ∈ 𝐶))
4	3	cbvralvw 3243	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 (𝑧‘𝑥) ∈ 𝐵 ↔ ∀𝑦 ∈ 𝐴 (𝑧‘𝑦) ∈ 𝐶)
5	4	anbi2i 634	. . 3 ⊢ ((𝑧 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑧‘𝑥) ∈ 𝐵) ↔ (𝑧 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑧‘𝑦) ∈ 𝐶))
6	5	abbii 2830	. 2 ⊢ {𝑧 ∣ (𝑧 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑧‘𝑥) ∈ 𝐵)} = {𝑧 ∣ (𝑧 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑧‘𝑦) ∈ 𝐶)}
7		dfixp 8898	. 2 ⊢ X𝑥 ∈ 𝐴 𝐵 = {𝑧 ∣ (𝑧 Fn 𝐴 ∧ ∀𝑥 ∈ 𝐴 (𝑧‘𝑥) ∈ 𝐵)}
8		dfixp 8898	. 2 ⊢ X𝑦 ∈ 𝐴 𝐶 = {𝑧 ∣ (𝑧 Fn 𝐴 ∧ ∀𝑦 ∈ 𝐴 (𝑧‘𝑦) ∈ 𝐶)}
9	6, 7, 8	3eqtr4i 2796	1 ⊢ X𝑥 ∈ 𝐴 𝐵 = X𝑦 ∈ 𝐴 𝐶

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143  {cab 2741  ∀wral 3079   Fn wfn 6533  ‘cfv 6538  Xcixp 8896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-iota 6494  df-fn 6541  df-fv 6546  df-ixp 8897

This theorem is referenced by:  funcpropd  17960  invfuc  18035  natpropd  18037  dprdw  20083  dprdwd  20084  ptuni2  23714  ptbasin  23715  ptbasfi  23719  ptpjopn  23750  ptclsg  23753  dfac14  23756  ptcnp  23760  ptcmplem2  24191  ptcmpg  24195  prdsxmslem2  24667  upixp  38361  rrxsnicc  46997  ioorrnopn  47002  ioorrnopnxr  47004  ovnsubadd  47269  hoidmvlelem4  47295  hoidmvle  47297  hspdifhsp  47313  hoiqssbllem2  47320  hspmbl  47326  hoimbl  47328  opnvonmbl  47331  ovnovollem3  47355