Metamath Proof Explorer


Theorem elrnrexdmb

Description: For any element in the range of a function there is an element in the domain of the function for which the function value is the element of the range. (Contributed by Alexander van der Vekens, 17-Dec-2017)

Ref Expression
Assertion elrnrexdmb
|- ( Fun F -> ( Y e. ran F <-> E. x e. dom F Y = ( F ` x ) ) )

Proof

Step Hyp Ref Expression
1 funfn
 |-  ( Fun F <-> F Fn dom F )
2 fvelrnb
 |-  ( F Fn dom F -> ( Y e. ran F <-> E. x e. dom F ( F ` x ) = Y ) )
3 1 2 sylbi
 |-  ( Fun F -> ( Y e. ran F <-> E. x e. dom F ( F ` x ) = Y ) )
4 eqcom
 |-  ( Y = ( F ` x ) <-> ( F ` x ) = Y )
5 4 rexbii
 |-  ( E. x e. dom F Y = ( F ` x ) <-> E. x e. dom F ( F ` x ) = Y )
6 3 5 bitr4di
 |-  ( Fun F -> ( Y e. ran F <-> E. x e. dom F Y = ( F ` x ) ) )