Theorem 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 AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$

Proof

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