Metamath Proof Explorer

Theorem mpteq2i

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

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

Proof

Step Hyp Ref Expression
1 mpteq2i.1 
 |-  B = C
2 1 a1i 
 |-  ( x e. A -> B = C )
3 2 mpteq2ia 
 |-  ( x e. A |-> B ) = ( x e. A |-> C )