Theorem funfvima2

Description: A function's value in an included preimage belongs to the image. (Contributed by NM, 3-Feb-1997)

	Ref	Expression
Assertion	funfvima2	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(B\in A\to F\left(B\right)\in F\left[A\right]\right)$$

Proof

Step	Hyp	Ref	Expression
1		funfvima	$$⊢\left(\mathrm{Fun}F\wedge B\in \mathrm{dom}F\right)\to \left(B\in A\to F\left(B\right)\in F\left[A\right]\right)$$
2	1	ex	$$⊢\mathrm{Fun}F\to \left(B\in \mathrm{dom}F\to \left(B\in A\to F\left(B\right)\in F\left[A\right]\right)\right)$$
3	2	com23	$$⊢\mathrm{Fun}F\to \left(B\in A\to \left(B\in \mathrm{dom}F\to F\left(B\right)\in F\left[A\right]\right)\right)$$
4	3	a2d	$$⊢\mathrm{Fun}F\to \left(\left(B\in A\to B\in \mathrm{dom}F\right)\to \left(B\in A\to F\left(B\right)\in F\left[A\right]\right)\right)$$
5		ssel	$$⊢A\subseteq \mathrm{dom}F\to \left(B\in A\to B\in \mathrm{dom}F\right)$$
6	4 5	impel	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(B\in A\to F\left(B\right)\in F\left[A\right]\right)$$