Theorem cocnvcnv2

Description: A composition is not affected by a double converse of its second argument. (Contributed by NM, 8-Oct-2007)

	Ref	Expression
Assertion	cocnvcnv2	$$⊢A\circ {B^{-1}}^{-1}=A\circ B$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	$$⊢{B^{-1}}^{-1}={B\upharpoonright }_{\mathrm{V}}$$
2	1	coeq2i	$$⊢A\circ {B^{-1}}^{-1}=A\circ \left({B\upharpoonright }_{\mathrm{V}}\right)$$
3		resco	$$⊢{\left(A\circ B\right)\upharpoonright }_{\mathrm{V}}=A\circ \left({B\upharpoonright }_{\mathrm{V}}\right)$$
4		relco	$$⊢\mathrm{Rel}\left(A\circ B\right)$$
5		dfrel3	$$⊢\mathrm{Rel}\left(A\circ B\right)\leftrightarrow {\left(A\circ B\right)\upharpoonright }_{\mathrm{V}}=A\circ B$$
6	4 5	mpbi	$$⊢{\left(A\circ B\right)\upharpoonright }_{\mathrm{V}}=A\circ B$$
7	2 3 6	3eqtr2i	$$⊢A\circ {B^{-1}}^{-1}=A\circ B$$