iinss

Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

		Ref	Expression
	Assertion	iinss	$⊢ \exists x \in A B \subseteq C \to ⋂_{x \in A} B \subseteq C$

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

Metamath Proof Explorer