Metamath Proof Explorer


Theorem cnvresid

Description: Converse of a restricted identity function. (Contributed by FL, 4-Mar-2007)

Ref Expression
Assertion cnvresid
|- `' ( _I |` A ) = ( _I |` A )

Proof

Step Hyp Ref Expression
1 cnvi
 |-  `' _I = _I
2 1 eqcomi
 |-  _I = `' _I
3 funi
 |-  Fun _I
4 funeq
 |-  ( _I = `' _I -> ( Fun _I <-> Fun `' _I ) )
5 3 4 mpbii
 |-  ( _I = `' _I -> Fun `' _I )
6 funcnvres
 |-  ( Fun `' _I -> `' ( _I |` A ) = ( `' _I |` ( _I " A ) ) )
7 imai
 |-  ( _I " A ) = A
8 1 7 reseq12i
 |-  ( `' _I |` ( _I " A ) ) = ( _I |` A )
9 6 8 eqtrdi
 |-  ( Fun `' _I -> `' ( _I |` A ) = ( _I |` A ) )
10 2 5 9 mp2b
 |-  `' ( _I |` A ) = ( _I |` A )