Theorem rescnvcnv

Description: The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	rescnvcnv	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	$$⊢{A^{-1}}^{-1}={A\upharpoonright }_{\mathrm{V}}$$
2	1	reseq1i	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={\left({A\upharpoonright }_{\mathrm{V}}\right)\upharpoonright }_B$$
3		resres	$$⊢{\left({A\upharpoonright }_{\mathrm{V}}\right)\upharpoonright }_B={A\upharpoonright }_{\left(\mathrm{V}\cap B\right)}$$
4		ssv	$$⊢B\subseteq \mathrm{V}$$
5		sseqin2	$$⊢B\subseteq \mathrm{V}\leftrightarrow \mathrm{V}\cap B=B$$
6	4 5	mpbi	$$⊢\mathrm{V}\cap B=B$$
7	6	reseq2i	$$⊢{A\upharpoonright }_{\left(\mathrm{V}\cap B\right)}={A\upharpoonright }_B$$
8	2 3 7	3eqtri	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A\upharpoonright }_B$$