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 syl6bb
 |-  ( 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 syl6bb
 |-  ( F Fn A -> ( B e. ran F <-> E. x e. A ( F ` x ) = B ) )