Theorem mpteq2da

Description: Slightly more general equality inference for the maps-to notation. (Contributed by FL, 14-Sep-2013) (Revised by Mario Carneiro, 16-Dec-2013)

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

Proof

Step	Hyp	Ref	Expression
1		mpteq2da.1	$$⊢Ⅎx\phi$$
2		mpteq2da.2	$$⊢\left(\phi \wedge x\in A\right)\to B=C$$
3		eqid	$$⊢A=A$$
4	3	ax-gen	$$⊢\forall xA=A$$
5	2	ex	$$⊢\phi \to \left(x\in A\to B=C\right)$$
6	1 5	ralrimi	$$⊢\phi \to \forall x\in AB=C$$
7		mpteq12f	$$⊢\left(\forall xA=A\wedge \forall x\in AB=C\right)\to \left(x\in A⟼B\right)=\left(x\in A⟼C\right)$$
8	4 6 7	sylancr	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in A⟼C\right)$$