Theorem imaexg

Description: The image of a set is a set. Theorem 3.17 of Monk1 p. 39. (Contributed by NM, 24-Jul-1995)

	Ref	Expression
Assertion	imaexg	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		imassrn	⊢ ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴
2		rnexg	⊢ ( 𝐴 ∈ 𝑉 → ran 𝐴 ∈ V )
3		ssexg	⊢ ( ( ( 𝐴 “ 𝐵 ) ⊆ ran 𝐴 ∧ ran 𝐴 ∈ V ) → ( 𝐴 “ 𝐵 ) ∈ V )
4	1 2 3	sylancr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 “ 𝐵 ) ∈ V )