Metamath Proof Explorer


Theorem mpteq1

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013)

Ref Expression
Assertion mpteq1 A = B x A C = x B C

Proof

Step Hyp Ref Expression
1 eqidd x A C = C
2 1 rgen x A C = C
3 mpteq12 A = B x A C = C x A C = x B C
4 2 3 mpan2 A = B x A C = x B C