Metamath Proof Explorer

Theorem rnco2

Description: The range of the composition of two classes. (Contributed by NM, 27-Mar-2008)

Ref Expression
Assertion rnco2 
|- ran ( A o. B ) = ( A " ran B )

Proof

Step Hyp Ref Expression
1 rnco 
 |-  ran ( A o. B ) = ran ( A |` ran B )
2 df-ima 
 |-  ( A " ran B ) = ran ( A |` ran B )
3 1 2 eqtr4i 
 |-  ran ( A o. B ) = ( A " ran B )