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 ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran 𝐴 = dom ◡ 𝐴
2	1	eqcomi	⊢ dom ◡ 𝐴 = ran 𝐴
3		dmcoeq	⊢ ( dom ◡ 𝐴 = ran 𝐴 → dom ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴 )
4	2 3	ax-mp	⊢ dom ( ◡ 𝐴 ∘ 𝐴 ) = dom 𝐴