Metamath Proof Explorer


Theorem xpeq2

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

Ref Expression
Assertion xpeq2 A=BC×A=C×B

Proof

Step Hyp Ref Expression
1 eleq2 A=ByAyB
2 1 anbi2d A=BxCyAxCyB
3 2 opabbidv A=Bxy|xCyA=xy|xCyB
4 df-xp C×A=xy|xCyA
5 df-xp C×B=xy|xCyB
6 3 4 5 3eqtr4g A=BC×A=C×B