Theorem mpteq12dv

Description: An equality inference for the maps-to notation. (Contributed by NM, 24-Aug-2011) (Revised by Mario Carneiro, 16-Dec-2013) Remove dependency on ax-10 , ax-12 . (Revised by SN and Gino Giotto, 1-Dec-2023)

	Ref	Expression
Hypotheses	mpteq12dv.1	|- ( ph -> A = C )
	mpteq12dv.2	|- ( ph -> B = D )
Assertion	mpteq12dv	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Proof

Step	Hyp	Ref	Expression
1		mpteq12dv.1	|- ( ph -> A = C )
2		mpteq12dv.2	|- ( ph -> B = D )
3	2	adantr	|- ( ( ph /\ x e. A ) -> B = D )
4	1 3	mpteq12dva	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )