Metamath Proof Explorer

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 \to (Y \in dom F \to \exists x \in ran F x = F (Y))$

Proof

Step	Hyp	Ref	Expression
1		fvelrn	$⊢ (Fun F \land Y \in dom F) \to F (Y) \in ran F$
2		eqid	$⊢ F (Y) = F (Y)$
3		eqeq1	$⊢ x = F (Y) \to (x = F (Y) \leftrightarrow F (Y) = F (Y))$
4	3	rspcev	$⊢ (F (Y) \in ran F \land F (Y) = F (Y)) \to \exists x \in ran F x = F (Y)$
5	1 2 4	sylancl	$⊢ (Fun F \land Y \in dom F) \to \exists x \in ran F x = F (Y)$
6	5	ex	$⊢ Fun F \to (Y \in dom F \to \exists x \in ran F x = F (Y))$