This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )