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	$$⊢Ⅎx\phi$$
	mpteq2dfa.2	$$⊢\left(\phi \wedge x\in A\right)\to B=C$$
Assertion	mpteq2dfa	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼C\right)$$

Proof

Step	Hyp	Ref	Expression
1		mpteq2dfa.1	$$⊢Ⅎx\phi$$
2		mpteq2dfa.2	$$⊢\left(\phi \wedge x\in A\right)\to B=C$$
3	1 2	mpteq2da	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼C\right)$$