Metamath Proof Explorer

Theorem dmcocnv1

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

Ref Expression
Assertion dmcocnv1 
|- dom ( `' 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 dmcoeq 
 |-  ( dom `' A = ran A -> dom ( `' A o. A ) = dom A )
4 2 3 ax-mp 
 |-  dom ( `' A o. A ) = dom A