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	$$⊢A^{-1}\left[\mathrm{ran}A\right]=\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		ssid	$$⊢\mathrm{ran}A\subseteq \mathrm{ran}A$$
2		cnvimassrndm	$$⊢\mathrm{ran}A\subseteq \mathrm{ran}A\to A^{-1}\left[\mathrm{ran}A\right]=\mathrm{dom}A$$
3	1 2	ax-mp	$$⊢A^{-1}\left[\mathrm{ran}A\right]=\mathrm{dom}A$$