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