Theorem funfvima2

Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997)

	Ref	Expression
Assertion	funfvima2	|- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )

Proof

Step	Hyp	Ref	Expression
1		funfvima	|- ( ( Fun F /\ B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )
2	1	ex	|- ( Fun F -> ( B e. dom F -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
3	2	com23	|- ( Fun F -> ( B e. A -> ( B e. dom F -> ( F ` B ) e. ( F " A ) ) ) )
4	3	a2d	|- ( Fun F -> ( ( B e. A -> B e. dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) ) )
5		ssel	|- ( A C_ dom F -> ( B e. A -> B e. dom F ) )
6	4 5	impel	|- ( ( Fun F /\ A C_ dom F ) -> ( B e. A -> ( F ` B ) e. ( F " A ) ) )