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