Theorem mptcnv

Description: The converse of a mapping function. (Contributed by Thierry Arnoux, 16-Jan-2017)

	Ref	Expression
Hypothesis	mptcnv.1	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(y\in C\wedge x=D\right)\right)$$
Assertion	mptcnv	$$⊢\phi \to {\left(x\in A⟼B\right)}^{-1}=\left(y\in C⟼D\right)$$

Proof

Step	Hyp	Ref	Expression
1		mptcnv.1	$$⊢\phi \to \left(\left(x\in A\wedge y=B\right)\leftrightarrow \left(y\in C\wedge x=D\right)\right)$$
2	1	opabbidv	$$⊢\phi \to \left\{⟨y,x⟩|\left(x\in A\wedge y=B\right)\right\}=\left\{⟨y,x⟩|\left(y\in C\wedge x=D\right)\right\}$$
3		df-mpt	$$⊢\left(x\in A⟼B\right)=\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}$$
4	3	cnveqi	$$⊢{\left(x\in A⟼B\right)}^{-1}={\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}}^{-1}$$
5		cnvopab	$$⊢{\left\{⟨x,y⟩|\left(x\in A\wedge y=B\right)\right\}}^{-1}=\left\{⟨y,x⟩|\left(x\in A\wedge y=B\right)\right\}$$
6	4 5	eqtri	$$⊢{\left(x\in A⟼B\right)}^{-1}=\left\{⟨y,x⟩|\left(x\in A\wedge y=B\right)\right\}$$
7		df-mpt	$$⊢\left(y\in C⟼D\right)=\left\{⟨y,x⟩|\left(y\in C\wedge x=D\right)\right\}$$
8	2 6 7	3eqtr4g	$$⊢\phi \to {\left(x\in A⟼B\right)}^{-1}=\left(y\in C⟼D\right)$$