Metamath Proof Explorer


Theorem cnvresid

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

Ref Expression
Assertion cnvresid ( I ↾ 𝐴 ) = ( I ↾ 𝐴 )

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 ↾ 𝐴 ) = ( I ↾ ( I “ 𝐴 ) ) )
7 imai ( I “ 𝐴 ) = 𝐴
8 1 7 reseq12i ( I ↾ ( I “ 𝐴 ) ) = ( I ↾ 𝐴 )
9 6 8 eqtrdi ( Fun I → ( I ↾ 𝐴 ) = ( I ↾ 𝐴 ) )
10 2 5 9 mp2b ( I ↾ 𝐴 ) = ( I ↾ 𝐴 )