This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem funimass5

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

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

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