Theorem xpeq2

Description: Equality theorem for Cartesian product. (Contributed by NM, 5-Jul-1994)

	Ref	Expression
Assertion	xpeq2	|- ( A = B -> ( C X. A ) = ( C X. B ) )

Proof

Step	Hyp	Ref	Expression
1		eleq2	|- ( A = B -> ( y e. A <-> y e. B ) )
2	1	anbi2d	|- ( A = B -> ( ( x e. C /\ y e. A ) <-> ( x e. C /\ y e. B ) ) )
3	2	opabbidv	|- ( A = B -> { <. x , y >. | ( x e. C /\ y e. A ) } = { <. x , y >. | ( x e. C /\ y e. B ) } )
4		df-xp	|- ( C X. A ) = { <. x , y >. | ( x e. C /\ y e. A ) }
5		df-xp	|- ( C X. B ) = { <. x , y >. | ( x e. C /\ y e. B ) }
6	3 4 5	3eqtr4g	|- ( A = B -> ( C X. A ) = ( C X. B ) )