Theorem fnfvelrnd

Description: A function's value belongs to its range. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	fnfvelrnd.1	$$⊢\phi \to FFnA$$
	fnfvelrnd.2	$$⊢\phi \to B\in A$$
Assertion	fnfvelrnd	$$⊢\phi \to F\left(B\right)\in \mathrm{ran}F$$

Proof

Step	Hyp	Ref	Expression
1		fnfvelrnd.1	$$⊢\phi \to FFnA$$
2		fnfvelrnd.2	$$⊢\phi \to B\in A$$
3		fnfvelrn	$$⊢\left(FFnA\wedge B\in A\right)\to F\left(B\right)\in \mathrm{ran}F$$
4	1 2 3	syl2anc	$$⊢\phi \to F\left(B\right)\in \mathrm{ran}F$$