Metamath Proof Explorer


Theorem cnvresid

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

Ref Expression
Assertion cnvresid I A -1 = I A

Proof

Step Hyp Ref Expression
1 cnvi I -1 = I
2 1 eqcomi I = I -1
3 funi Fun I
4 funeq I = I -1 Fun I Fun I -1
5 3 4 mpbii I = I -1 Fun I -1
6 funcnvres Fun I -1 I A -1 = I -1 I A
7 imai I A = A
8 1 7 reseq12i I -1 I A = I A
9 6 8 eqtrdi Fun I -1 I A -1 = I A
10 2 5 9 mp2b I A -1 = I A