Description: Converse of a restricted identity function. (Contributed by FL, 4Mar2007)
Ref  Expression  

Assertion  cnvresid   `' ( _I ` A ) = ( _I ` A ) 
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  syl6eq   ( Fun `' _I > `' ( _I ` A ) = ( _I ` A ) ) 
10  2 5 9  mp2b   `' ( _I ` A ) = ( _I ` A ) 