Metamath Proof Explorer

Theorem imacnvcnv

Description: The image of the double converse of a class. (Contributed by NM, 8-Apr-2007)

Ref Expression
Assertion imacnvcnv 
|- ( `' `' A " B ) = ( A " B )

Proof

Step Hyp Ref Expression
1 rescnvcnv 
 |-  ( `' `' A |` B ) = ( A |` B )
2 1 rneqi 
 |-  ran ( `' `' A |` B ) = ran ( A |` B )
3 df-ima 
 |-  ( `' `' A " B ) = ran ( `' `' A |` B )
4 df-ima 
 |-  ( A " B ) = ran ( A |` B )
5 2 3 4 3eqtr4i 
 |-  ( `' `' A " B ) = ( A " B )