Metamath Proof Explorer


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 )