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	⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴

Proof

Step	Hyp	Ref	Expression
1		ssv	⊢ 𝐵 ⊆ V
2		imass2	⊢ ( 𝐵 ⊆ V → ( 𝐴 “ 𝐵 ) ⊆ ( 𝐴 “ V ) )
3	1 2	ax-mp	⊢ ( 𝐴 “ 𝐵 ) ⊆ ( 𝐴 “ V )
4		dfrn4	⊢ ran 𝐴 = ( 𝐴 “ V )
5	3 4	sseqtrri	⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴