Theorem fnfvelrn

Description: A function's value belongs to its range. (Contributed by NM, 15-Oct-1996)

	Ref	Expression
Assertion	fnfvelrn	$$⊢\left(FFnA\wedge B\in A\right)\to F\left(B\right)\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fvelrn	$$⊢\left(\mathrm{Fun}F\wedge B\in \mathrm{dom}F\right)\to F\left(B\right)\in \mathrm{ran}F$$
2	1	funfni	$$⊢\left(FFnA\wedge B\in A\right)\to F\left(B\right)\in \mathrm{ran}F$$