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, 4May2005)
Ref  Expression  

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