This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )