Theorem cnvimarndm

Description: The preimage of the range of a class is equal to the domain of the class. (Contributed by Jeff Hankins, 15-Jul-2009) (Proof shortened by BJ, 29-Sep-2026)

	Ref	Expression
Assertion	cnvimarndm	⊢ ( ◡ 𝐴 “ ran 𝐴 ) = dom 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssid	⊢ ran 𝐴 ⊆ ran 𝐴
2		cnvimassrndm	⊢ ( ran 𝐴 ⊆ ran 𝐴 → ( ◡ 𝐴 “ ran 𝐴 ) = dom 𝐴 )
3	1 2	ax-mp	⊢ ( ◡ 𝐴 “ ran 𝐴 ) = dom 𝐴