This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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