Metamath Proof Explorer

Theorem mpteq1i

Description: An equality theorem for the maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis mpteq1i.1 
|- A = B
Assertion mpteq1i 
|- ( x e. A |-> C ) = ( x e. B |-> C )

Proof

Step Hyp Ref Expression
1 mpteq1i.1 
 |-  A = B
2 mpteq1 
 |-  ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )
3 1 2 ax-mp 
 |-  ( x e. A |-> C ) = ( x e. B |-> C )