Metamath Proof Explorer


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 B -1 -1 = A B

Proof

Step Hyp Ref Expression
1 cnvcnv2 B -1 -1 = B V
2 1 coeq2i A B -1 -1 = A B V
3 resco A B V = A B V
4 relco Rel A B
5 dfrel3 Rel A B A B V = A B
6 4 5 mpbi A B V = A B
7 2 3 6 3eqtr2i A B -1 -1 = A B