Theorem imadmrn

Description: The image of the domain of a class is equal to its range. (Contributed by NM, 14-Aug-1994) (Proof shortened by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	imadmrn	$$⊢A\left[\mathrm{dom}A\right]=\mathrm{ran}A$$

Proof

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