This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } ) ) )