Theorem cnvresid

Description: A restricted identity relation is equal to its converse. (Contributed by FL, 4-Mar-2007) Remove dependency on ax-12 and shorten. (Revised by BJ, 1-Nov-2026)

	Ref	Expression
Assertion	cnvresid	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$

Proof

Step	Hyp	Ref	Expression
1		cnvin	$$⊢{\left(\mathrm{I}\cap \left(A\times A\right)\right)}^{-1}={\mathrm{I}}^{-1}\cap {\left(A\times A\right)}^{-1}$$
2		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
3		cnvxp	$$⊢{\left(A\times A\right)}^{-1}=A\times A$$
4	2 3	ineq12i	$$⊢{\mathrm{I}}^{-1}\cap {\left(A\times A\right)}^{-1}=\mathrm{I}\cap \left(A\times A\right)$$
5	1 4	eqtri	$$⊢{\left(\mathrm{I}\cap \left(A\times A\right)\right)}^{-1}=\mathrm{I}\cap \left(A\times A\right)$$
6		idinxpresid	$$⊢\mathrm{I}\cap \left(A\times A\right)={\mathrm{I}\upharpoonright }_A$$
7	6	cnveqi	$$⊢{\left(\mathrm{I}\cap \left(A\times A\right)\right)}^{-1}={\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}$$
8	5 7 6	3eqtr3i	$$⊢{\left({\mathrm{I}\upharpoonright }_A\right)}^{-1}={\mathrm{I}\upharpoonright }_A$$