Metamath Proof Explorer


Theorem cocnvcnv1

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

Ref Expression
Assertion cocnvcnv1 A-1-1B=AB

Proof

Step Hyp Ref Expression
1 cnvcnv2 A-1-1=AV
2 1 coeq1i A-1-1B=AVB
3 ssv ranBV
4 cores ranBVAVB=AB
5 3 4 ax-mp AVB=AB
6 2 5 eqtri A-1-1B=AB