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

Metamath Proof Explorer

Theorem cnvcnvres

Description: The double converse of the restriction of a class. (Contributed by NM, 3-Jun-2007)

Ref Expression
Assertion cnvcnvres ⊢ A ↾ B -1 -1 = A -1 -1 ↾ B

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ⁡ A ↾ B
2 dfrel2 ⊢ Rel ⁡ A ↾ B ↔ A ↾ B -1 -1 = A ↾ B
3 1 2 mpbi ⊢ A ↾ B -1 -1 = A ↾ B
4 rescnvcnv ⊢ A -1 -1 ↾ B = A ↾ B
5 3 4 eqtr4i ⊢ A ↾ B -1 -1 = A -1 -1 ↾ B