Theorem funfvima3

Description: A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004)

	Ref	Expression
Assertion	funfvima3	|- ( ( Fun F /\ F C_ G ) -> ( A e. dom F -> ( F ` A ) e. ( G " { A } ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( F C_ G -> ( <. A , ( F ` A ) >. e. F -> <. A , ( F ` A ) >. e. G ) )
2		funfvop	|- ( ( Fun F /\ A e. dom F ) -> <. A , ( F ` A ) >. e. F )
3	1 2	impel	|- ( ( F C_ G /\ ( Fun F /\ A e. dom F ) ) -> <. A , ( F ` A ) >. e. G )
4		sneq	|- ( x = A -> { x } = { A } )
5	4	imaeq2d	|- ( x = A -> ( G " { x } ) = ( G " { A } ) )
6	5	eleq2d	|- ( x = A -> ( ( F ` A ) e. ( G " { x } ) <-> ( F ` A ) e. ( G " { A } ) ) )
7		opeq1	|- ( x = A -> <. x , ( F ` A ) >. = <. A , ( F ` A ) >. )
8	7	eleq1d	|- ( x = A -> ( <. x , ( F ` A ) >. e. G <-> <. A , ( F ` A ) >. e. G ) )
9		vex	|- x e. _V
10		fvex	|- ( F ` A ) e. _V
11	9 10	elimasn	|- ( ( F ` A ) e. ( G " { x } ) <-> <. x , ( F ` A ) >. e. G )
12	6 8 11	vtoclbg	|- ( A e. dom F -> ( ( F ` A ) e. ( G " { A } ) <-> <. A , ( F ` A ) >. e. G ) )
13	12	ad2antll	|- ( ( F C_ G /\ ( Fun F /\ A e. dom F ) ) -> ( ( F ` A ) e. ( G " { A } ) <-> <. A , ( F ` A ) >. e. G ) )
14	3 13	mpbird	|- ( ( F C_ G /\ ( Fun F /\ A e. dom F ) ) -> ( F ` A ) e. ( G " { A } ) )
15	14	exp32	|- ( F C_ G -> ( Fun F -> ( A e. dom F -> ( F ` A ) e. ( G " { A } ) ) ) )
16	15	impcom	|- ( ( Fun F /\ F C_ G ) -> ( A e. dom F -> ( F ` A ) e. ( G " { A } ) ) )