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

Metamath Proof Explorer

Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

Ref Expression
Assertion fvelrnb 
|- ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )

Proof

Step Hyp Ref Expression
1 fnrnfv 
 |-  ( F Fn A -> ran F = { y | E. x e. A y = ( F ` x ) } )
2 1 eleq2d 
 |-  ( F Fn A -> ( B e. ran F <-> B e. { y | E. x e. A y = ( F ` x ) } ) )
3 fvex 
 |-  ( F ` x ) e. _V
4 eleq1 
 |-  ( ( F ` x ) = B -> ( ( F ` x ) e. _V <-> B e. _V ) )
5 3 4 mpbii 
 |-  ( ( F ` x ) = B -> B e. _V )
6 5 rexlimivw 
 |-  ( E. x e. A ( F ` x ) = B -> B e. _V )
7 eqeq1 
 |-  ( y = B -> ( y = ( F ` x ) <-> B = ( F ` x ) ) )
8 eqcom 
 |-  ( B = ( F ` x ) <-> ( F ` x ) = B )
9 7 8 bitrdi 
 |-  ( y = B -> ( y = ( F ` x ) <-> ( F ` x ) = B ) )
10 9 rexbidv 
 |-  ( y = B -> ( E. x e. A y = ( F ` x ) <-> E. x e. A ( F ` x ) = B ) )
11 6 10 elab3 
 |-  ( B e. { y | E. x e. A y = ( F ` x ) } <-> E. x e. A ( F ` x ) = B )
12 2 11 bitrdi 
 |-  ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )