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 𝐵 = 𝐶
Assertion mpteq2i ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐶 )

Proof

Step Hyp Ref Expression
1 mpteq2i.1 𝐵 = 𝐶
2 1 a1i ( 𝑥𝐴𝐵 = 𝐶 )
3 2 mpteq2ia ( 𝑥𝐴𝐵 ) = ( 𝑥𝐴𝐶 )