Theorem fnfvimad

Description: A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	fnfvimad.1	$$⊢\phi \to FFnA$$
	fnfvimad.2	$$⊢\phi \to B\in A$$
	fnfvimad.3	$$⊢\phi \to B\in C$$
Assertion	fnfvimad	$$⊢\phi \to F\left(B\right)\in F\left[C\right]$$

Proof

Step	Hyp	Ref	Expression
1		fnfvimad.1	$$⊢\phi \to FFnA$$
2		fnfvimad.2	$$⊢\phi \to B\in A$$
3		fnfvimad.3	$$⊢\phi \to B\in C$$
4		inss2	$$⊢A\cap C\subseteq C$$
5		imass2	$$⊢A\cap C\subseteq C\to F\left[A\cap C\right]\subseteq F\left[C\right]$$
6	4 5	ax-mp	$$⊢F\left[A\cap C\right]\subseteq F\left[C\right]$$
7		inss1	$$⊢A\cap C\subseteq A$$
8	7	a1i	$$⊢\phi \to A\cap C\subseteq A$$
9	2 3	elind	$$⊢\phi \to B\in \left(A\cap C\right)$$
10		fnfvima	$$⊢\left(FFnA\wedge A\cap C\subseteq A\wedge B\in \left(A\cap C\right)\right)\to F\left(B\right)\in F\left[A\cap C\right]$$
11	1 8 9 10	syl3anc	$$⊢\phi \to F\left(B\right)\in F\left[A\cap C\right]$$
12	6 11	sselid	$$⊢\phi \to F\left(B\right)\in F\left[C\right]$$