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 F -> `' ( `' F |` A ) = ( F |` ( `' F " A ) ) )

Proof

Step	Hyp	Ref	Expression
1		funcnvcnv	|- ( Fun F -> Fun `' `' F )
2		funcnvres	|- ( Fun `' `' F -> `' ( `' F |` A ) = ( `' `' F |` ( `' F " A ) ) )
3	1 2	syl	|- ( Fun F -> `' ( `' F |` A ) = ( `' `' F |` ( `' F " A ) ) )
4		funrel	|- ( Fun F -> Rel F )
5		dfrel2	|- ( Rel F <-> `' `' F = F )
6	4 5	sylib	|- ( Fun F -> `' `' F = F )
7	6	reseq1d	|- ( Fun F -> ( `' `' F |` ( `' F " A ) ) = ( F |` ( `' F " A ) ) )
8	3 7	eqtrd	|- ( Fun F -> `' ( `' F |` A ) = ( F |` ( `' F " A ) ) )