Metamath Proof Explorer

Theorem mpteq1

Description: An equality theorem for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013) (Proof shortened by SN, 11-Nov-2024)

Ref Expression
Assertion mpteq1 
|- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( A = B -> A = B )
2 eqidd 
 |-  ( A = B -> C = C )
3 1 2 mpteq12dv 
 |-  ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )