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 A B = x A C

Proof

Step Hyp Ref Expression
1 mpteq2i.1 B = C
2 1 a1i x A B = C
3 2 mpteq2ia x A B = x A C