Metamath Proof Explorer

Theorem mpteq12

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

Ref Expression
Assertion mpteq12 
|- ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Proof

Step Hyp Ref Expression
1 ax-5 
 |-  ( A = C -> A. x A = C )
2 mpteq12f 
 |-  ( ( A. x A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )
3 1 2 sylan 
 |-  ( ( A = C /\ A. x e. A B = D ) -> ( x e. A |-> B ) = ( x e. C |-> D ) )