Theorem afvelrnb0

Description: A member of a function's range is a value of the function, only one direction of implication of fvelrnb . (Contributed by Alexander van der Vekens, 1-Jun-2017)

	Ref	Expression
Assertion	afvelrnb0	$$⊢FFnA\to \left(B\in \mathrm{ran}F\to \exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnrnafv	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}$$
2	1	eleq2d	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow B\in \left\{y|\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}\right)$$
3		eqeq1	$$⊢y=B\to \left(y=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\leftrightarrow B=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right)$$
4		eqcom	$$⊢B=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B$$
5	3 4	bitrdi	$$⊢y=B\to \left(y=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\leftrightarrow \left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B\right)$$
6	5	rexbidv	$$⊢y=B\to \left(\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\leftrightarrow \exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B\right)$$
7	6	elabg	$$⊢B\in \left\{y|\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}\to \left(B\in \left\{y|\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}\leftrightarrow \exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B\right)$$
8	7	ibi	$$⊢B\in \left\{y|\exists x\in Ay=\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)\right\}\to \exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B$$
9	2 8	biimtrdi	$$⊢FFnA\to \left(B\in \mathrm{ran}F\to \exists x\in A\left(F\mathrm{\text{'}\text{'}\text{'}}x\right)=B\right)$$