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 ) = ( `' `' A |` B )

Proof

Step Hyp Ref Expression
1 relres
 |-  Rel ( A |` B )
2 dfrel2
 |-  ( Rel ( A |` B ) <-> `' `' ( A |` B ) = ( A |` B ) )
3 1 2 mpbi
 |-  `' `' ( A |` B ) = ( A |` B )
4 rescnvcnv
 |-  ( `' `' A |` B ) = ( A |` B )
5 3 4 eqtr4i
 |-  `' `' ( A |` B ) = ( `' `' A |` B )