Theorem fnimafnex

Description: The functional image of a function value exists. (Contributed by RP, 31-Oct-2024)

	Ref	Expression
Hypothesis	fnimafnex.f	⊢ 𝐹 Fn 𝐵
Assertion	fnimafnex	⊢ ( 𝐹 “ ( 𝐺 ‘ 𝐴 ) ) ∈ V

Proof

Step	Hyp	Ref	Expression
1		fnimafnex.f	⊢ 𝐹 Fn 𝐵
2		fnfun	⊢ ( 𝐹 Fn 𝐵 → Fun 𝐹 )
3	1 2	ax-mp	⊢ Fun 𝐹
4		fvex	⊢ ( 𝐺 ‘ 𝐴 ) ∈ V
5		funimaexg	⊢ ( ( Fun 𝐹 ∧ ( 𝐺 ‘ 𝐴 ) ∈ V ) → ( 𝐹 “ ( 𝐺 ‘ 𝐴 ) ) ∈ V )
6	3 4 5	mp2an	⊢ ( 𝐹 “ ( 𝐺 ‘ 𝐴 ) ) ∈ V