Metamath Proof Explorer

Theorem rncocnv1

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

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

Proof

Step Hyp Ref Expression
1 df-rn 
 |-  ran A = dom `' A
2 1 eqcomi 
 |-  dom `' A = ran A
3 rncoeq 
 |-  ( dom `' A = ran A -> ran ( `' A o. A ) = ran `' A )
4 2 3 ax-mp 
 |-  ran ( `' A o. A ) = ran `' A
5 dfdm4 
 |-  dom A = ran `' A
6 4 5 eqtr4i 
 |-  ran ( `' A o. A ) = dom A