Theorem iinssd

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

	Ref	Expression
Hypotheses	iinssd.1	$$⊢\phi \to X\in A$$
	iinssd.2	$$⊢x=X\to B=D$$
	iinssd.3	$$⊢\phi \to D\subseteq C$$
Assertion	iinssd	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iinssd.1	$$⊢\phi \to X\in A$$
2		iinssd.2	$$⊢x=X\to B=D$$
3		iinssd.3	$$⊢\phi \to D\subseteq C$$
4	2	sseq1d	$$⊢x=X\to \left(B\subseteq C\leftrightarrow D\subseteq C\right)$$
5	4	rspcev	$$⊢\left(X\in A\wedge D\subseteq C\right)\to \exists x\in AB\subseteq C$$
6	1 3 5	syl2anc	$$⊢\phi \to \exists x\in AB\subseteq C$$
7		iinss	$$⊢\exists x\in AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$
8	6 7	syl	$$⊢\phi \to \bigcap _{x\in A}B\subseteq C$$