Theorem funfvima2d

Description: A function's value in a preimage belongs to the image. (Contributed by Stanislas Polu, 9-Mar-2020) (Revised by AV, 23-Mar-2024)

	Ref	Expression
Hypothesis	funfvima2d.1	$$⊢\phi \to F:A⟶B$$
Assertion	funfvima2d	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)\in F\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		funfvima2d.1	$$⊢\phi \to F:A⟶B$$
2	1	ffund	$$⊢\phi \to \mathrm{Fun}F$$
3		ssidd	$$⊢\phi \to A\subseteq A$$
4	1	fdmd	$$⊢\phi \to \mathrm{dom}F=A$$
5	3 4	sseqtrrd	$$⊢\phi \to A\subseteq \mathrm{dom}F$$
6		funfvima2	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(X\in A\to F\left(X\right)\in F\left[A\right]\right)$$
7	2 5 6	syl2anc	$$⊢\phi \to \left(X\in A\to F\left(X\right)\in F\left[A\right]\right)$$
8	7	imp	$$⊢\left(\phi \wedge X\in A\right)\to F\left(X\right)\in F\left[A\right]$$