Metamath Proof Explorer


Theorem xpeq2

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

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

Proof

Step Hyp Ref Expression
1 eleq2 A = B y A y B
2 1 anbi2d A = B x C y A x C y B
3 2 opabbidv A = B x y | x C y A = x y | x C y B
4 df-xp C × A = x y | x C y A
5 df-xp C × B = x y | x C y B
6 3 4 5 3eqtr4g A = B C × A = C × B