fint

Description: Function into an intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

		Ref	Expression
	Hypothesis	fint.1	$⊢ B \neq \emptyset$
	Assertion	fint	$⊢ F : A ⟶ ⋂ B \leftrightarrow \forall x \in B F : A ⟶ x$

Step	Hyp	Ref	Expression
1		fint.1	$⊢ B \neq \emptyset$
2		ssint	$⊢ ran F \subseteq ⋂ B \leftrightarrow \forall x \in B ran F \subseteq x$
3	2	anbi2i	$⊢ (F Fn A \land ran F \subseteq ⋂ B) \leftrightarrow (F Fn A \land \forall x \in B ran F \subseteq x)$
4		r19.28zv	$⊢ B \neq \emptyset \to (\forall x \in B (F Fn A \land ran F \subseteq x) \leftrightarrow (F Fn A \land \forall x \in B ran F \subseteq x))$
5	1 4	ax-mp	$⊢ \forall x \in B (F Fn A \land ran F \subseteq x) \leftrightarrow (F Fn A \land \forall x \in B ran F \subseteq x)$
6	3 5	bitr4i	$⊢ (F Fn A \land ran F \subseteq ⋂ B) \leftrightarrow \forall x \in B (F Fn A \land ran F \subseteq x)$
7		df-f	$⊢ F : A ⟶ ⋂ B \leftrightarrow (F Fn A \land ran F \subseteq ⋂ B)$
8		df-f	$⊢ F : A ⟶ x \leftrightarrow (F Fn A \land ran F \subseteq x)$
9	8	ralbii	$⊢ \forall x \in B F : A ⟶ x \leftrightarrow \forall x \in B (F Fn A \land ran F \subseteq x)$
10	6 7 9	3bitr4i	$⊢ F : A ⟶ ⋂ B \leftrightarrow \forall x \in B F : A ⟶ x$

Metamath Proof Explorer