# Metamath Proof Explorer

## Theorem cbvixp

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 20-Jun-2011)

Ref Expression
Hypotheses cbvixp.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
cbvixp.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
cbvixp.3 ${⊢}{x}={y}\to {B}={C}$
Assertion cbvixp ${⊢}\underset{{x}\in {A}}{⨉}{B}=\underset{{y}\in {A}}{⨉}{C}$

### Proof

Step Hyp Ref Expression
1 cbvixp.1 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}{B}$
2 cbvixp.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{C}$
3 cbvixp.3 ${⊢}{x}={y}\to {B}={C}$
4 1 nfel2 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}$
5 2 nfel2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {C}$
6 fveq2 ${⊢}{x}={y}\to {f}\left({x}\right)={f}\left({y}\right)$
7 6 3 eleq12d ${⊢}{x}={y}\to \left({f}\left({x}\right)\in {B}↔{f}\left({y}\right)\in {C}\right)$
8 4 5 7 cbvralw ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}↔\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {C}$
9 8 anbi2i ${⊢}\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)↔\left({f}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {C}\right)$
10 9 abbii ${⊢}\left\{{f}|\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}=\left\{{f}|\left({f}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {C}\right)\right\}$
11 dfixp ${⊢}\underset{{x}\in {A}}{⨉}{B}=\left\{{f}|\left({f}Fn{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)\right\}$
12 dfixp ${⊢}\underset{{y}\in {A}}{⨉}{C}=\left\{{f}|\left({f}Fn{A}\wedge \forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in {C}\right)\right\}$
13 10 11 12 3eqtr4i ${⊢}\underset{{x}\in {A}}{⨉}{B}=\underset{{y}\in {A}}{⨉}{C}$