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 )