Theorem mpteq12da

Description: An equality inference for the maps-to notation. (Contributed by Glauco Siliprandi, 23-Oct-2021) Remove dependency on ax-10 . (Revised by SN, 11-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mpteq12da.1	$$⊢Ⅎx\phi$$
2		mpteq12da.2	$$⊢\phi \to A=C$$
3		mpteq12da.3	$$⊢\left(\phi \wedge x\in A\right)\to B=D$$
4		nfv	$$⊢Ⅎy\phi$$
5	3	eqeq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(y=B\leftrightarrow y=D\right)$$
6	5	pm5.32da	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in A\wedge y=D\right)\right)$$
7	2	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in C\right)$$
8	7	anbi1d	$$⊢\phi \to \left(\left(x\in A\wedge y=D\right)\leftrightarrow \left(x\in C\wedge y=D\right)\right)$$
9	6 8	bitrd	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in C\wedge y=D\right)\right)$$
10	1 4 9	opabbid	$$⊢\phi \to \left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{⟨x,y⟩|\left(x\in C\wedge y=D\right)\right\}$$
11		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
12		df-mpt	$$⊢\left(x\in C⟼D\right)=\left\{⟨x,y⟩|\left(x\in C\wedge y=D\right)\right\}$$
13	10 11 12	3eqtr4g	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in C⟼D\right)$$