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