Theorem funcnvres2

Description: The converse of a restriction of the converse of a function equals the function restricted to the image of its converse. (Contributed by NM, 4-May-2005)

	Ref	Expression
Assertion	funcnvres2	⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐴 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcnvcnv	⊢ ( Fun 𝐹 → Fun ◡ ◡ 𝐹 )
2		funcnvres	⊢ ( Fun ◡ ◡ 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐴 ) = ( ◡ ◡ 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) )
3	1 2	syl	⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐴 ) = ( ◡ ◡ 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) )
4		funrel	⊢ ( Fun 𝐹 → Rel 𝐹 )
5		dfrel2	⊢ ( Rel 𝐹 ↔ ◡ ◡ 𝐹 = 𝐹 )
6	4 5	sylib	⊢ ( Fun 𝐹 → ◡ ◡ 𝐹 = 𝐹 )
7	6	reseq1d	⊢ ( Fun 𝐹 → ( ◡ ◡ 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) )
8	3 7	eqtrd	⊢ ( Fun 𝐹 → ◡ ( ◡ 𝐹 ↾ 𝐴 ) = ( 𝐹 ↾ ( ◡ 𝐹 “ 𝐴 ) ) )