Metamath Proof Explorer


Theorem xpeq1

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

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

Proof

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