Theorem mpteq12dva

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017) Remove dependency on ax-10 , ax-12 . (Revised by SN, 11-Nov-2024)

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

Proof

Step	Hyp	Ref	Expression
1		mpteq12dv.1	$$⊢\phi \to A=C$$
2		mpteq12dva.2	$$⊢\left(\phi \wedge x\in A\right)\to B=D$$
3	2	eqeq2d	$$⊢\left(\phi \wedge x\in A\right)\to \left(y=B\leftrightarrow y=D\right)$$
4	3	pm5.32da	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in A\wedge y=D\right)\right)$$
5	1	eleq2d	$$⊢\phi \to \left(x\in A\leftrightarrow x\in C\right)$$
6	5	anbi1d	$$⊢\phi \to \left(\left(x\in A\wedge y=D\right)\leftrightarrow \left(x\in C\wedge y=D\right)\right)$$
7	4 6	bitrd	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(x\in C\wedge y=D\right)\right)$$
8	7	opabbidv	$$⊢\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\}$$
9		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
10		df-mpt	$$⊢\left(x\in C⟼D\right)=\left\{⟨x,y⟩|\left(x\in C\wedge y=D\right)\right\}$$
11	8 9 10	3eqtr4g	$$⊢\phi \to \left(x\in A⟼B\right)=\left(x\in C⟼D\right)$$