Theorem eldmrexrn

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

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

Proof

Step	Hyp	Ref	Expression
1		fvelrn	|- ( ( Fun F /\ Y e. dom F ) -> ( F ` Y ) e. ran F )
2		eqid	|- ( F ` Y ) = ( F ` Y )
3		eqeq1	|- ( x = ( F ` Y ) -> ( x = ( F ` Y ) <-> ( F ` Y ) = ( F ` Y ) ) )
4	3	rspcev	|- ( ( ( F ` Y ) e. ran F /\ ( F ` Y ) = ( F ` Y ) ) -> E. x e. ran F x = ( F ` Y ) )
5	1 2 4	sylancl	|- ( ( Fun F /\ Y e. dom F ) -> E. x e. ran F x = ( F ` Y ) )
6	5	ex	|- ( Fun F -> ( Y e. dom F -> E. x e. ran F x = ( F ` Y ) ) )