ixpeq1

Description: Equality theorem for infinite Cartesian product. (Contributed by NM, 29-Sep-2006)

		Ref	Expression
	Assertion	ixpeq1	$⊢ A = B \to \underset{x \in A}{⨉} C = \underset{x \in B}{⨉} C$

Step	Hyp	Ref	Expression
1		fneq2	$⊢ A = B \to (f Fn A \leftrightarrow f Fn B)$
2		raleq	$⊢ A = B \to (\forall x \in A f (x) \in C \leftrightarrow \forall x \in B f (x) \in C)$
3	1 2	anbi12d	$⊢ A = B \to ((f Fn A \land \forall x \in A f (x) \in C) \leftrightarrow (f Fn B \land \forall x \in B f (x) \in C))$
4	3	abbidv	$⊢ A = B \to \{f \| (f Fn A \land \forall x \in A f (x) \in C)\} = \{f \| (f Fn B \land \forall x \in B f (x) \in C)\}$
5		dfixp	$⊢ \underset{x \in A}{⨉} C = \{f \| (f Fn A \land \forall x \in A f (x) \in C)\}$
6		dfixp	$⊢ \underset{x \in B}{⨉} C = \{f \| (f Fn B \land \forall x \in B f (x) \in C)\}$
7	4 5 6	3eqtr4g	$⊢ A = B \to \underset{x \in A}{⨉} C = \underset{x \in B}{⨉} C$

Metamath Proof Explorer