funfvima2

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

		Ref	Expression
	Assertion	funfvima2	$⊢ (Fun F \land A \subseteq dom F) \to (B \in A \to F (B) \in F [A])$

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

Metamath Proof Explorer