Theorem altxpeq2

Description: Equality for alternate Cartesian products. (Contributed by Scott Fenton, 24-Mar-2012)

	Ref	Expression
Assertion	altxpeq2	|- ( A = B -> ( C XX. A ) = ( C XX. B ) )

Proof

Step	Hyp	Ref	Expression
1		rexeq	|- ( A = B -> ( E. y e. A z = << x , y >> <-> E. y e. B z = << x , y >> ) )
2	1	rexbidv	|- ( A = B -> ( E. x e. C E. y e. A z = << x , y >> <-> E. x e. C E. y e. B z = << x , y >> ) )
3	2	abbidv	|- ( A = B -> { z | E. x e. C E. y e. A z = << x , y >> } = { z | E. x e. C E. y e. B z = << x , y >> } )
4		df-altxp	|- ( C XX. A ) = { z | E. x e. C E. y e. A z = << x , y >> }
5		df-altxp	|- ( C XX. B ) = { z | E. x e. C E. y e. B z = << x , y >> }
6	3 4 5	3eqtr4g	|- ( A = B -> ( C XX. A ) = ( C XX. B ) )