Metamath Proof Explorer


Theorem xpeq1

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

Ref Expression
Assertion xpeq1 A=BA×C=B×C

Proof

Step Hyp Ref Expression
1 eleq2 A=BxAxB
2 1 anbi1d A=BxAyCxByC
3 2 opabbidv A=Bxy|xAyC=xy|xByC
4 df-xp A×C=xy|xAyC
5 df-xp B×C=xy|xByC
6 3 4 5 3eqtr4g A=BA×C=B×C