fnfvimad

Description: A function's value belongs to the image. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Step	Hyp	Ref	Expression
1		fnfvimad.1	$⊢ φ \to F Fn A$
2		fnfvimad.2	$⊢ φ \to B \in A$
3		fnfvimad.3	$⊢ φ \to B \in C$
4		inss2	$⊢ A \cap C \subseteq C$
5		imass2	$⊢ A \cap C \subseteq C \to F [A \cap C] \subseteq F [C]$
6	4 5	ax-mp	$⊢ F [A \cap C] \subseteq F [C]$
7		inss1	$⊢ A \cap C \subseteq A$
8	7	a1i	$⊢ φ \to A \cap C \subseteq A$
9	2 3	elind	$⊢ φ \to B \in (A \cap C)$
10		fnfvima	$⊢ (F Fn A \land A \cap C \subseteq A \land B \in (A \cap C)) \to F (B) \in F [A \cap C]$
11	1 8 9 10	syl3anc	$⊢ φ \to F (B) \in F [A \cap C]$
12	6 11	sselid	$⊢ φ \to F (B) \in F [C]$

Metamath Proof Explorer