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

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	⊢ ◡ ◡ 𝐴 = ( 𝐴 ↾ V )
2	1	coeq1i	⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( ( 𝐴 ↾ V ) ∘ 𝐵 )
3		ssv	⊢ ran 𝐵 ⊆ V
4		cores	⊢ ( ran 𝐵 ⊆ V → ( ( 𝐴 ↾ V ) ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 ) )
5	3 4	ax-mp	⊢ ( ( 𝐴 ↾ V ) ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )
6	2 5	eqtri	⊢ ( ◡ ◡ 𝐴 ∘ 𝐵 ) = ( 𝐴 ∘ 𝐵 )