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	|- F/ x ph
	mpteq12df.2	|- ( ph -> A = C )
	mpteq12df.3	|- ( ph -> B = D )
Assertion	mpteq12df	|- ( ph -> ( x e. A |-> B ) = ( x e. C |-> D ) )

Proof

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