Theorem imassrn

Description: Any image by a class is included in the range of the class. Theorem 3.16(xi) of Monk1 p. 39. (Contributed by NM, 31-Mar-1995) (Proof shortened by BJ, 27-Sep-2026)

	Ref	Expression
Assertion	imassrn	$$⊢A\left[B\right]\subseteq \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		ssv	$$⊢B\subseteq \mathrm{V}$$
2		imass2	$$⊢B\subseteq \mathrm{V}\to A\left[B\right]\subseteq A\left[\mathrm{V}\right]$$
3	1 2	ax-mp	$$⊢A\left[B\right]\subseteq A\left[\mathrm{V}\right]$$
4		dfrn4	$$⊢\mathrm{ran}A=A\left[\mathrm{V}\right]$$
5	3 4	sseqtrri	$$⊢A\left[B\right]\subseteq \mathrm{ran}A$$