Metamath Proof Explorer


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 ) ) )