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 ( 𝐴 𝐵 ) = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 cnvcnv2 𝐵 = ( 𝐵 ↾ V )
2 1 coeq2i ( 𝐴 𝐵 ) = ( 𝐴 ∘ ( 𝐵 ↾ V ) )
3 resco ( ( 𝐴𝐵 ) ↾ V ) = ( 𝐴 ∘ ( 𝐵 ↾ V ) )
4 relco Rel ( 𝐴𝐵 )
5 dfrel3 ( Rel ( 𝐴𝐵 ) ↔ ( ( 𝐴𝐵 ) ↾ V ) = ( 𝐴𝐵 ) )
6 4 5 mpbi ( ( 𝐴𝐵 ) ↾ V ) = ( 𝐴𝐵 )
7 2 3 6 3eqtr2i ( 𝐴 𝐵 ) = ( 𝐴𝐵 )