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