Theorem fnfvimad

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

	Ref	Expression
Hypotheses	fnfvimad.1	|- ( ph -> F Fn A )
	fnfvimad.2	|- ( ph -> B e. A )
	fnfvimad.3	|- ( ph -> B e. C )
Assertion	fnfvimad	|- ( ph -> ( F ` B ) e. ( F " C ) )

Proof

Step	Hyp	Ref	Expression
1		fnfvimad.1	|- ( ph -> F Fn A )
2		fnfvimad.2	|- ( ph -> B e. A )
3		fnfvimad.3	|- ( ph -> B e. C )
4		inss2	|- ( A i^i C ) C_ C
5		imass2	|- ( ( A i^i C ) C_ C -> ( F " ( A i^i C ) ) C_ ( F " C ) )
6	4 5	ax-mp	|- ( F " ( A i^i C ) ) C_ ( F " C )
7		inss1	|- ( A i^i C ) C_ A
8	7	a1i	|- ( ph -> ( A i^i C ) C_ A )
9	2 3	elind	|- ( ph -> B e. ( A i^i C ) )
10		fnfvima	|- ( ( F Fn A /\ ( A i^i C ) C_ A /\ B e. ( A i^i C ) ) -> ( F ` B ) e. ( F " ( A i^i C ) ) )
11	1 8 9 10	syl3anc	|- ( ph -> ( F ` B ) e. ( F " ( A i^i C ) ) )
12	6 11	sselid	|- ( ph -> ( F ` B ) e. ( F " C ) )