Metamath Proof Explorer

Theorem ixpeq1i

Description: Equality inference for infinite Cartesian product. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypothesis ixpeq1i.1 
|- A = B
Assertion ixpeq1i 
|- X_ x e. A C = X_ x e. B C

Proof

Step Hyp Ref Expression
1 ixpeq1i.1 
 |-  A = B
2 1 eleq2i 
 |-  ( x e. A <-> x e. B )
3 2 abbii 
 |-  { x | x e. A } = { x | x e. B }
4 3 fneq2i 
 |-  ( f Fn { x | x e. A } <-> f Fn { x | x e. B } )
5 2 imbi1i 
 |-  ( ( x e. A -> ( f ` x ) e. C ) <-> ( x e. B -> ( f ` x ) e. C ) )
6 5 ralbii2 
 |-  ( A. x e. A ( f ` x ) e. C <-> A. x e. B ( f ` x ) e. C )
7 4 6 anbi12i 
 |-  ( ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) <-> ( f Fn { x | x e. B } /\ A. x e. B ( f ` x ) e. C ) )
8 7 abbii 
 |-  { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) } = { f | ( f Fn { x | x e. B } /\ A. x e. B ( f ` x ) e. C ) }
9 df-ixp 
 |-  X_ x e. A C = { f | ( f Fn { x | x e. A } /\ A. x e. A ( f ` x ) e. C ) }
10 df-ixp 
 |-  X_ x e. B C = { f | ( f Fn { x | x e. B } /\ A. x e. B ( f ` x ) e. C ) }
11 8 9 10 3eqtr4i 
 |-  X_ x e. A C = X_ x e. B C