Metamath Proof Explorer

Theorem cnvcnv

Description: The double converse of a class strips out all elements that are not ordered pairs. (Contributed by NM, 8-Dec-2003) (Proof shortened by BJ, 26-Nov-2021)

Ref Expression
Assertion cnvcnv 
|- `' `' A = ( A i^i ( _V X. _V ) )

Proof

Step Hyp Ref Expression
1 cnvin 
 |-  `' ( `' A i^i `' ( _V X. _V ) ) = ( `' `' A i^i `' `' ( _V X. _V ) )
2 cnvin 
 |-  `' ( A i^i ( _V X. _V ) ) = ( `' A i^i `' ( _V X. _V ) )
3 2 cnveqi 
 |-  `' `' ( A i^i ( _V X. _V ) ) = `' ( `' A i^i `' ( _V X. _V ) )
4 relcnv 
 |-  Rel `' `' A
5 df-rel 
 |-  ( Rel `' `' A <-> `' `' A C_ ( _V X. _V ) )
6 4 5 mpbi 
 |-  `' `' A C_ ( _V X. _V )
7 relxp 
 |-  Rel ( _V X. _V )
8 dfrel2 
 |-  ( Rel ( _V X. _V ) <-> `' `' ( _V X. _V ) = ( _V X. _V ) )
9 7 8 mpbi 
 |-  `' `' ( _V X. _V ) = ( _V X. _V )
10 6 9 sseqtrri 
 |-  `' `' A C_ `' `' ( _V X. _V )
11 dfss 
 |-  ( `' `' A C_ `' `' ( _V X. _V ) <-> `' `' A = ( `' `' A i^i `' `' ( _V X. _V ) ) )
12 10 11 mpbi 
 |-  `' `' A = ( `' `' A i^i `' `' ( _V X. _V ) )
13 1 3 12 3eqtr4ri 
 |-  `' `' A = `' `' ( A i^i ( _V X. _V ) )
14 relinxp 
 |-  Rel ( A i^i ( _V X. _V ) )
15 dfrel2 
 |-  ( Rel ( A i^i ( _V X. _V ) ) <-> `' `' ( A i^i ( _V X. _V ) ) = ( A i^i ( _V X. _V ) ) )
16 14 15 mpbi 
 |-  `' `' ( A i^i ( _V X. _V ) ) = ( A i^i ( _V X. _V ) )
17 13 16 eqtri 
 |-  `' `' A = ( A i^i ( _V X. _V ) )