Theorem xpeq1

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

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

Proof

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