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 o. `' `' B ) = ( A o. B )

Proof

Step Hyp Ref Expression
1 cnvcnv2
 |-  `' `' B = ( B |` _V )
2 1 coeq2i
 |-  ( A o. `' `' B ) = ( A o. ( B |` _V ) )
3 resco
 |-  ( ( A o. B ) |` _V ) = ( A o. ( B |` _V ) )
4 relco
 |-  Rel ( A o. B )
5 dfrel3
 |-  ( Rel ( A o. B ) <-> ( ( A o. B ) |` _V ) = ( A o. B ) )
6 4 5 mpbi
 |-  ( ( A o. B ) |` _V ) = ( A o. B )
7 2 3 6 3eqtr2i
 |-  ( A o. `' `' B ) = ( A o. B )