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

Proof

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