Theorem riinn0

Description: Relative intersection of a nonempty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	riinn0	$$⊢\left(\forall x\in XS\subseteq A\wedge X\ne \varnothing \right)\to A\cap \bigcap _{x\in X}S=\bigcap _{x\in X}S$$

Proof

Step	Hyp	Ref	Expression
1		incom	$$⊢A\cap \bigcap _{x\in X}S=\bigcap _{x\in X}S\cap A$$
2		r19.2z	$$⊢\left(X\ne \varnothing \wedge \forall x\in XS\subseteq A\right)\to \exists x\in XS\subseteq A$$
3	2	ancoms	$$⊢\left(\forall x\in XS\subseteq A\wedge X\ne \varnothing \right)\to \exists x\in XS\subseteq A$$
4		iinss	$$⊢\exists x\in XS\subseteq A\to \bigcap _{x\in X}S\subseteq A$$
5	3 4	syl	$$⊢\left(\forall x\in XS\subseteq A\wedge X\ne \varnothing \right)\to \bigcap _{x\in X}S\subseteq A$$
6		df-ss	$$⊢\bigcap _{x\in X}S\subseteq A\leftrightarrow \bigcap _{x\in X}S\cap A=\bigcap _{x\in X}S$$
7	5 6	sylib	$$⊢\left(\forall x\in XS\subseteq A\wedge X\ne \varnothing \right)\to \bigcap _{x\in X}S\cap A=\bigcap _{x\in X}S$$
8	1 7	syl5eq	$$⊢\left(\forall x\in XS\subseteq A\wedge X\ne \varnothing \right)\to A\cap \bigcap _{x\in X}S=\bigcap _{x\in X}S$$