Theorem fnfvima

Description: The function value of an operand in a set is contained in the image of that set, using the Fn abbreviation. (Contributed by Stefan O'Rear, 10-Mar-2015)

	Ref	Expression
Assertion	fnfvima	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S ) )

Proof

Step	Hyp	Ref	Expression
1		fnfun	|- ( F Fn A -> Fun F )
2	1	3ad2ant1	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> Fun F )
3		simp2	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> S C_ A )
4		fndm	|- ( F Fn A -> dom F = A )
5	4	3ad2ant1	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> dom F = A )
6	3 5	sseqtrrd	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> S C_ dom F )
7	2 6	jca	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( Fun F /\ S C_ dom F ) )
8		simp3	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> X e. S )
9		funfvima2	|- ( ( Fun F /\ S C_ dom F ) -> ( X e. S -> ( F ` X ) e. ( F " S ) ) )
10	7 8 9	sylc	|- ( ( F Fn A /\ S C_ A /\ X e. S ) -> ( F ` X ) e. ( F " S ) )