Theorem ixpeq12dv

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

	Ref	Expression
Hypotheses	ixpeq12dv.1	|- ( ph -> A = B )
	ixpeq12dv.2	|- ( ph -> C = D )
Assertion	ixpeq12dv	|- ( ph -> X_ x e. A C = X_ x e. B D )

Proof

Step	Hyp	Ref	Expression
1		ixpeq12dv.1	|- ( ph -> A = B )
2		ixpeq12dv.2	|- ( ph -> C = D )
3	1	eleq2d	|- ( ph -> ( x e. A <-> x e. B ) )
4	3	abbidv	|- ( ph -> { x | x e. A } = { x | x e. B } )
5	4	fneq2d	|- ( ph -> ( t Fn { x | x e. A } <-> t Fn { x | x e. B } ) )
6	3	imbi1d	|- ( ph -> ( ( x e. A -> ( t ` x ) e. C ) <-> ( x e. B -> ( t ` x ) e. C ) ) )
7	6	albidv	|- ( ph -> ( A. x ( x e. A -> ( t ` x ) e. C ) <-> A. x ( x e. B -> ( t ` x ) e. C ) ) )
8		df-ral	|- ( A. x e. A ( t ` x ) e. C <-> A. x ( x e. A -> ( t ` x ) e. C ) )
9		df-ral	|- ( A. x e. B ( t ` x ) e. C <-> A. x ( x e. B -> ( t ` x ) e. C ) )
10	7 8 9	3bitr4g	|- ( ph -> ( A. x e. A ( t ` x ) e. C <-> A. x e. B ( t ` x ) e. C ) )
11	5 10	anbi12d	|- ( ph -> ( ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) <-> ( t Fn { x | x e. B } /\ A. x e. B ( t ` x ) e. C ) ) )
12	11	abbidv	|- ( ph -> { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) } = { t | ( t Fn { x | x e. B } /\ A. x e. B ( t ` x ) e. C ) } )
13		df-ixp	|- X_ x e. A C = { t | ( t Fn { x | x e. A } /\ A. x e. A ( t ` x ) e. C ) }
14		df-ixp	|- X_ x e. B C = { t | ( t Fn { x | x e. B } /\ A. x e. B ( t ` x ) e. C ) }
15	12 13 14	3eqtr4g	|- ( ph -> X_ x e. A C = X_ x e. B C )
16	2	ixpeq2dv	|- ( ph -> X_ x e. B C = X_ x e. B D )
17	15 16	eqtrd	|- ( ph -> X_ x e. A C = X_ x e. B D )