Metamath Proof Explorer

Theorem fvelrn

Description: A function's value belongs to its range. (Contributed by NM, 14-Oct-1996)

Ref Expression
Assertion fvelrn 
|- ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )

Proof

Step Hyp Ref Expression
1 eleq1 
 |-  ( x = A -> ( x e. dom F <-> A e. dom F ) )
2 1 anbi2d 
 |-  ( x = A -> ( ( Fun F /\ x e. dom F ) <-> ( Fun F /\ A e. dom F ) ) )
3 fveq2 
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
4 3 eleq1d 
 |-  ( x = A -> ( ( F ` x ) e. ran F <-> ( F ` A ) e. ran F ) )
5 2 4 imbi12d 
 |-  ( x = A -> ( ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F ) <-> ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F ) ) )
6 funfvop 
 |-  ( ( Fun F /\ x e. dom F ) -> <. x , ( F ` x ) >. e. F )
7 vex 
 |-  x e. _V
8 opeq1 
 |-  ( y = x -> <. y , ( F ` x ) >. = <. x , ( F ` x ) >. )
9 8 eleq1d 
 |-  ( y = x -> ( <. y , ( F ` x ) >. e. F <-> <. x , ( F ` x ) >. e. F ) )
10 7 9 spcev 
 |-  ( <. x , ( F ` x ) >. e. F -> E. y <. y , ( F ` x ) >. e. F )
11 6 10 syl 
 |-  ( ( Fun F /\ x e. dom F ) -> E. y <. y , ( F ` x ) >. e. F )
12 fvex 
 |-  ( F ` x ) e. _V
13 12 elrn2 
 |-  ( ( F ` x ) e. ran F <-> E. y <. y , ( F ` x ) >. e. F )
14 11 13 sylibr 
 |-  ( ( Fun F /\ x e. dom F ) -> ( F ` x ) e. ran F )
15 5 14 vtoclg 
 |-  ( A e. dom F -> ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F ) )
16 15 anabsi7 
 |-  ( ( Fun F /\ A e. dom F ) -> ( F ` A ) e. ran F )