Theorem ixpeq1

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

	Ref	Expression
Assertion	ixpeq1	|- ( A = B -> X_ x e. A C = X_ x e. B C )

Proof

Step	Hyp	Ref	Expression
1		fneq2	|- ( A = B -> ( f Fn A <-> f Fn B ) )
2		raleq	|- ( A = B -> ( A. x e. A ( f ` x ) e. C <-> A. x e. B ( f ` x ) e. C ) )
3	1 2	anbi12d	|- ( A = B -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. C ) <-> ( f Fn B /\ A. x e. B ( f ` x ) e. C ) ) )
4	3	abbidv	|- ( A = B -> { f | ( f Fn A /\ A. x e. A ( f ` x ) e. C ) } = { f | ( f Fn B /\ A. x e. B ( f ` x ) e. C ) } )
5		dfixp	|- X_ x e. A C = { f | ( f Fn A /\ A. x e. A ( f ` x ) e. C ) }
6		dfixp	|- X_ x e. B C = { f | ( f Fn B /\ A. x e. B ( f ` x ) e. C ) }
7	4 5 6	3eqtr4g	|- ( A = B -> X_ x e. A C = X_ x e. B C )