cbvixpv

Description: Change bound variable in an indexed Cartesian product. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Hypothesis	cbvixpv.1	$⊢ x = y \to B = C$
	Assertion	cbvixpv	$⊢ \underset{x \in A}{⨉} B = \underset{y \in A}{⨉} C$

Step	Hyp	Ref	Expression
1		cbvixpv.1	$⊢ x = y \to B = C$
2		fveq2	$⊢ x = y \to z (x) = z (y)$
3	2 1	eleq12d	$⊢ x = y \to (z (x) \in B \leftrightarrow z (y) \in C)$
4	3	cbvralvw	$⊢ \forall x \in A z (x) \in B \leftrightarrow \forall y \in A z (y) \in C$
5	4	anbi2i	$⊢ (z Fn A \land \forall x \in A z (x) \in B) \leftrightarrow (z Fn A \land \forall y \in A z (y) \in C)$
6	5	abbii	$⊢ \{z \| (z Fn A \land \forall x \in A z (x) \in B)\} = \{z \| (z Fn A \land \forall y \in A z (y) \in C)\}$
7		dfixp	$⊢ \underset{x \in A}{⨉} B = \{z \| (z Fn A \land \forall x \in A z (x) \in B)\}$
8		dfixp	$⊢ \underset{y \in A}{⨉} C = \{z \| (z Fn A \land \forall y \in A z (y) \in C)\}$
9	6 7 8	3eqtr4i	$⊢ \underset{x \in A}{⨉} B = \underset{y \in A}{⨉} C$

Metamath Proof Explorer