Theorem cnvcnvres

Description: The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007)

	Ref	Expression
Assertion	cnvcnvres	$$⊢{{\left({A\upharpoonright }_B\right)}^{-1}}^{-1}={{A^{-1}}^{-1}\upharpoonright }_B$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)$$
2		dfrel2	$$⊢\mathrm{Rel}\left({A\upharpoonright }_B\right)\leftrightarrow {{\left({A\upharpoonright }_B\right)}^{-1}}^{-1}={A\upharpoonright }_B$$
3	1 2	mpbi	$$⊢{{\left({A\upharpoonright }_B\right)}^{-1}}^{-1}={A\upharpoonright }_B$$
4		rescnvcnv	$$⊢{{A^{-1}}^{-1}\upharpoonright }_B={A\upharpoonright }_B$$
5	3 4	eqtr4i	$$⊢{{\left({A\upharpoonright }_B\right)}^{-1}}^{-1}={{A^{-1}}^{-1}\upharpoonright }_B$$