Theorem fvelrnb

Description: A member of a function's range is a value of the function. (Contributed by NM, 31-Oct-1995)

	Ref	Expression
Assertion	fvelrnb	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow \exists x\in AF\left(x\right)=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	$$⊢FFnA\to \mathrm{ran}F=\left\{y|\exists x\in Ay=F\left(x\right)\right\}$$
2	1	eleq2d	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow B\in \left\{y|\exists x\in Ay=F\left(x\right)\right\}\right)$$
3		fvex	$$⊢F\left(x\right)\in \mathrm{V}$$
4		eleq1	$$⊢F\left(x\right)=B\to \left(F\left(x\right)\in \mathrm{V}\leftrightarrow B\in \mathrm{V}\right)$$
5	3 4	mpbii	$$⊢F\left(x\right)=B\to B\in \mathrm{V}$$
6	5	rexlimivw	$$⊢\exists x\in AF\left(x\right)=B\to B\in \mathrm{V}$$
7		eqeq1	$$⊢y=B\to \left(y=F\left(x\right)\leftrightarrow B=F\left(x\right)\right)$$
8		eqcom	$$⊢B=F\left(x\right)\leftrightarrow F\left(x\right)=B$$
9	7 8	bitrdi	$$⊢y=B\to \left(y=F\left(x\right)\leftrightarrow F\left(x\right)=B\right)$$
10	9	rexbidv	$$⊢y=B\to \left(\exists x\in Ay=F\left(x\right)\leftrightarrow \exists x\in AF\left(x\right)=B\right)$$
11	6 10	elab3	$$⊢B\in \left\{y|\exists x\in Ay=F\left(x\right)\right\}\leftrightarrow \exists x\in AF\left(x\right)=B$$
12	2 11	bitrdi	$$⊢FFnA\to \left(B\in \mathrm{ran}F\leftrightarrow \exists x\in AF\left(x\right)=B\right)$$