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 )