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

Proof

Step Hyp Ref Expression
1 cnvcnv2 
 |-  `' `' A = ( A |` _V )
2 1 coeq1i 
 |-  ( `' `' A o. B ) = ( ( A |` _V ) o. B )
3 ssv 
 |-  ran B C_ _V
4 cores 
 |-  ( ran B C_ _V -> ( ( A |` _V ) o. B ) = ( A o. B ) )
5 3 4 ax-mp 
 |-  ( ( A |` _V ) o. B ) = ( A o. B )
6 2 5 eqtri 
 |-  ( `' `' A o. B ) = ( A o. B )