Metamath Proof Explorer

Theorem dmcocnv2

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

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

Proof

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