Metamath Proof Explorer


Theorem mpteq12df

Description: An equality inference for the maps-to notation. Compare mpteq12dv . (Contributed by Scott Fenton, 8-Aug-2013) (Revised by Mario Carneiro, 11-Dec-2016) (Proof shortened by SN, 11-Nov-2024)

Ref Expression
Hypotheses mpteq12df.1 𝑥 𝜑
mpteq12df.2 ( 𝜑𝐴 = 𝐶 )
mpteq12df.3 ( 𝜑𝐵 = 𝐷 )
Assertion mpteq12df ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐶𝐷 ) )

Proof

Step Hyp Ref Expression
1 mpteq12df.1 𝑥 𝜑
2 mpteq12df.2 ( 𝜑𝐴 = 𝐶 )
3 mpteq12df.3 ( 𝜑𝐵 = 𝐷 )
4 3 adantr ( ( 𝜑𝑥𝐴 ) → 𝐵 = 𝐷 )
5 1 2 4 mpteq12da ( 𝜑 → ( 𝑥𝐴𝐵 ) = ( 𝑥𝐶𝐷 ) )