Theorem rescnvcnv

Description: The restriction of the double converse of a class. (Contributed by NM, 8-Apr-2007) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	rescnvcnv	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	⊢ ◡ ◡ 𝐴 = ( 𝐴 ↾ V )
2	1	reseq1i	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( ( 𝐴 ↾ V ) ↾ 𝐵 )
3		resres	⊢ ( ( 𝐴 ↾ V ) ↾ 𝐵 ) = ( 𝐴 ↾ ( V ∩ 𝐵 ) )
4		ssv	⊢ 𝐵 ⊆ V
5		sseqin2	⊢ ( 𝐵 ⊆ V ↔ ( V ∩ 𝐵 ) = 𝐵 )
6	4 5	mpbi	⊢ ( V ∩ 𝐵 ) = 𝐵
7	6	reseq2i	⊢ ( 𝐴 ↾ ( V ∩ 𝐵 ) ) = ( 𝐴 ↾ 𝐵 )
8	2 3 7	3eqtri	⊢ ( ◡ ◡ 𝐴 ↾ 𝐵 ) = ( 𝐴 ↾ 𝐵 )