Theorem mpteq2dfa

Description: Slightly more general equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 21-Dec-2024)

	Ref	Expression
Hypotheses	mpteq2dfa.1	|- F/ x ph
	mpteq2dfa.2	|- ( ( ph /\ x e. A ) -> B = C )
Assertion	mpteq2dfa	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Proof

Step	Hyp	Ref	Expression
1		mpteq2dfa.1	|- F/ x ph
2		mpteq2dfa.2	|- ( ( ph /\ x e. A ) -> B = C )
3	1 2	mpteq2da	|- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )