Theorem fnimafnex

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

	Ref	Expression
Hypothesis	fnimafnex.f	|- F Fn B
Assertion	fnimafnex	|- ( F " ( G ` A ) ) e. _V

Proof

Step	Hyp	Ref	Expression
1		fnimafnex.f	|- F Fn B
2		fnfun	|- ( F Fn B -> Fun F )
3	1 2	ax-mp	|- Fun F
4		fvex	|- ( G ` A ) e. _V
5		funimaexg	|- ( ( Fun F /\ ( G ` A ) e. _V ) -> ( F " ( G ` A ) ) e. _V )
6	3 4 5	mp2an	|- ( F " ( G ` A ) ) e. _V