Theorem funimass5

Description: A subclass of a preimage in terms of function values. (Contributed by NM, 15-May-2007)

	Ref	Expression
Assertion	funimass5	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(A\subseteq F^{-1}\left[B\right]\leftrightarrow \forall x\in AF\left(x\right)\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		funimass3	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(F\left[A\right]\subseteq B\leftrightarrow A\subseteq F^{-1}\left[B\right]\right)$$
2		funimass4	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(F\left[A\right]\subseteq B\leftrightarrow \forall x\in AF\left(x\right)\in B\right)$$
3	1 2	bitr3d	$$⊢\left(\mathrm{Fun}F\wedge A\subseteq \mathrm{dom}F\right)\to \left(A\subseteq F^{-1}\left[B\right]\leftrightarrow \forall x\in AF\left(x\right)\in B\right)$$