Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 cnvcnv2 
 |-  `' `' A = ( A |` _V )
2 1 reseq1i 
 |-  ( `' `' A |` B ) = ( ( A |` _V ) |` B )
3 resres 
 |-  ( ( A |` _V ) |` B ) = ( A |` ( _V i^i B ) )
4 ssv 
 |-  B C_ _V
5 sseqin2 
 |-  ( B C_ _V <-> ( _V i^i B ) = B )
6 4 5 mpbi 
 |-  ( _V i^i B ) = B
7 6 reseq2i 
 |-  ( A |` ( _V i^i B ) ) = ( A |` B )
8 2 3 7 3eqtri 
 |-  ( `' `' A |` B ) = ( A |` B )