Metamath Proof Explorer


Theorem mpoeq12

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

Ref Expression
Assertion mpoeq12 A = C B = D x A , y B E = x C , y D E

Proof

Step Hyp Ref Expression
1 eqid E = E
2 1 rgenw y B E = E
3 2 jctr B = D B = D y B E = E
4 3 ralrimivw B = D x A B = D y B E = E
5 mpoeq123 A = C x A B = D y B E = E x A , y B E = x C , y D E
6 4 5 sylan2 A = C B = D x A , y B E = x C , y D E