Theorem fnimafnex

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

	Ref	Expression
Hypothesis	fnimafnex.f	$$⊢FFnB$$
Assertion	fnimafnex	$$⊢F\left[G\left(A\right)\right]\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		fnimafnex.f	$$⊢FFnB$$
2		fnfun	$$⊢FFnB\to \mathrm{Fun}F$$
3	1 2	ax-mp	$$⊢\mathrm{Fun}F$$
4		fvex	$$⊢G\left(A\right)\in \mathrm{V}$$
5		funimaexg	$$⊢\left(\mathrm{Fun}F\wedge G\left(A\right)\in \mathrm{V}\right)\to F\left[G\left(A\right)\right]\in \mathrm{V}$$
6	3 4 5	mp2an	$$⊢F\left[G\left(A\right)\right]\in \mathrm{V}$$