Metamath Proof Explorer

Theorem rncocnv2

Description: The range of a class precomposed with its converse is equal to its range. (Contributed by BJ, 25-Oct-2026)

Ref Expression
Assertion rncocnv2 
|- ran ( A o. `' A ) = ran A

Proof

Step Hyp Ref Expression
1 dfdm4 
 |-  dom A = ran `' A
2 rncoeq 
 |-  ( dom A = ran `' A -> ran ( A o. `' A ) = ran A )
3 1 2 ax-mp 
 |-  ran ( A o. `' A ) = ran A