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 )