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 ( 𝐴𝐵 ) = ( 𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 relres Rel ( 𝐴𝐵 )
2 dfrel2 ( Rel ( 𝐴𝐵 ) ↔ ( 𝐴𝐵 ) = ( 𝐴𝐵 ) )
3 1 2 mpbi ( 𝐴𝐵 ) = ( 𝐴𝐵 )
4 rescnvcnv ( 𝐴𝐵 ) = ( 𝐴𝐵 )
5 3 4 eqtr4i ( 𝐴𝐵 ) = ( 𝐴𝐵 )