Theorem iinss2

Description: An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	iinss2	$$⊢x\in A\to \bigcap _{x\in A}B\subseteq B$$

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		rsp	$$⊢\forall x\in Ay\in B\to \left(x\in A\to y\in B\right)$$
4	3	com12	$$⊢x\in A\to \left(\forall x\in Ay\in B\to y\in B\right)$$
5	2 4	syl5bi	$$⊢x\in A\to \left(y\in \bigcap _{x\in A}B\to y\in B\right)$$
6	5	ssrdv	$$⊢x\in A\to \bigcap _{x\in A}B\subseteq B$$