iinssf

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Hypothesis	iinssf.1	$⊢ \underline{Ⅎ} x C$
	Assertion	iinssf	$⊢ \exists x \in A B \subseteq C \to ⋂_{x \in A} B \subseteq C$

Step	Hyp	Ref	Expression
1		iinssf.1	$⊢ \underline{Ⅎ} x C$
2		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} B \leftrightarrow \forall x \in A y \in B)$
3	2	elv	$⊢ y \in ⋂_{x \in A} B \leftrightarrow \forall x \in A y \in B$
4		ssel	$⊢ B \subseteq C \to (y \in B \to y \in C)$
5	4	reximi	$⊢ \exists x \in A B \subseteq C \to \exists x \in A (y \in B \to y \in C)$
6	1	nfcri	$⊢ Ⅎ x y \in C$
7	6	r19.36vf	$⊢ \exists x \in A (y \in B \to y \in C) \to (\forall x \in A y \in B \to y \in C)$
8	5 7	syl	$⊢ \exists x \in A B \subseteq C \to (\forall x \in A y \in B \to y \in C)$
9	3 8	biimtrid	$⊢ \exists x \in A B \subseteq C \to (y \in ⋂_{x \in A} B \to y \in C)$
10	9	ssrdv	$⊢ \exists x \in A B \subseteq C \to ⋂_{x \in A} B \subseteq C$

Metamath Proof Explorer