cbvixp

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

	Ref	Expression
Hypotheses	cbvixp.1	$⊢ \underline{Ⅎ} y B$
	cbvixp.2	$⊢ \underline{Ⅎ} x C$
	cbvixp.3	$⊢ x = y \to B = C$
Assertion	cbvixp	$⊢ \underset{x \in A}{⨉} B = \underset{y \in A}{⨉} C$

Step	Hyp	Ref	Expression
1		cbvixp.1	$⊢ \underline{Ⅎ} y B$
2		cbvixp.2	$⊢ \underline{Ⅎ} x C$
3		cbvixp.3	$⊢ x = y \to B = C$
4	1	nfel2	$⊢ Ⅎ y f (x) \in B$
5	2	nfel2	$⊢ Ⅎ x f (y) \in C$
6		fveq2	$⊢ x = y \to f (x) = f (y)$
7	6 3	eleq12d	$⊢ x = y \to (f (x) \in B \leftrightarrow f (y) \in C)$
8	4 5 7	cbvralw	$⊢ \forall x \in A f (x) \in B \leftrightarrow \forall y \in A f (y) \in C$
9	8	anbi2i	$⊢ (f Fn A \land \forall x \in A f (x) \in B) \leftrightarrow (f Fn A \land \forall y \in A f (y) \in C)$
10	9	abbii	$⊢ \{f \| (f Fn A \land \forall x \in A f (x) \in B)\} = \{f \| (f Fn A \land \forall y \in A f (y) \in C)\}$
11		dfixp	$⊢ \underset{x \in A}{⨉} B = \{f \| (f Fn A \land \forall x \in A f (x) \in B)\}$
12		dfixp	$⊢ \underset{y \in A}{⨉} C = \{f \| (f Fn A \land \forall y \in A f (y) \in C)\}$
13	10 11 12	3eqtr4i	$⊢ \underset{x \in A}{⨉} B = \underset{y \in A}{⨉} C$

Metamath Proof Explorer