Metamath Proof Explorer


Theorem mpteq12dv

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 16-Dec-2013) Drop ax-10 while shortening its proof. (Revised by Steven Nguyen and Gino Giotto, 1-Dec-2023)

Ref Expression
Hypotheses mpteq12dv.1 φ A = C
mpteq12dv.2 φ B = D
Assertion mpteq12dv φ x A B = x C D

Proof

Step Hyp Ref Expression
1 mpteq12dv.1 φ A = C
2 mpteq12dv.2 φ B = D
3 nfv x φ
4 3 1 2 mpteq12df φ x A B = x C D