Metamath Proof Explorer

Theorem cnvcnv2

Description: The double converse of a class equals its restriction to the universe. (Contributed by NM, 8-Oct-2007)

Ref Expression
Assertion cnvcnv2 
|- `' `' A = ( A |` _V )

Proof

Step Hyp Ref Expression
1 cnvcnv 
 |-  `' `' A = ( A i^i ( _V X. _V ) )
2 df-res 
 |-  ( A |` _V ) = ( A i^i ( _V X. _V ) )
3 1 2 eqtr4i 
 |-  `' `' A = ( A |` _V )