Theorem fafvelrn

Description: A function's value belongs to its codomain, analogous to ffvelrn . (Contributed by Alexander van der Vekens, 25-May-2017)

	Ref	Expression
Assertion	fafvelrn	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		ffn	$$⊢F:A⟶B\to FFnA$$
2		fnafvelrn	$$⊢\left(FFnA\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F$$
3	1 2	sylan	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F$$
4		frn	$$⊢F:A⟶B\to \mathrm{ran}F\subseteq B$$
5	4	sseld	$$⊢F:A⟶B\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in B\right)$$
6	5	adantr	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(\left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in \mathrm{ran}F\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in B\right)$$
7	3 6	mpd	$$⊢\left(F:A⟶B\wedge C\in A\right)\to \left(F\mathrm{\text{'}\text{'}\text{'}}C\right)\in B$$