Theorem altxpeq1

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

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

Proof

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