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

Proof

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		fvelrnb	$⊢ F Fn dom F \to (Y \in ran F \leftrightarrow \exists x \in dom F F (x) = Y)$
3	1 2	sylbi	$⊢ Fun F \to (Y \in ran F \leftrightarrow \exists x \in dom F F (x) = Y)$
4		eqcom	$⊢ Y = F (x) \leftrightarrow F (x) = Y$
5	4	rexbii	$⊢ \exists x \in dom F Y = F (x) \leftrightarrow \exists x \in dom F F (x) = Y$
6	3 5	bitr4di	$⊢ Fun F \to (Y \in ran F \leftrightarrow \exists x \in dom F Y = F (x))$