Theorem iinssf

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

	Ref	Expression
Hypothesis	iinssf.1	$$⊢\underset{\_}{Ⅎ}xC$$
Assertion	iinssf	$$⊢\exists x\in AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$

Proof

Step	Hyp	Ref	Expression
1		iinssf.1	$$⊢\underset{\_}{Ⅎ}xC$$
2		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B\right)$$
3	2	elv	$$⊢y\in \bigcap _{x\in A}B\leftrightarrow \forall x\in Ay\in B$$
4		ssel	$$⊢B\subseteq C\to \left(y\in B\to y\in C\right)$$
5	4	reximi	$$⊢\exists x\in AB\subseteq C\to \exists x\in A\left(y\in B\to y\in C\right)$$
6	1	nfcri	$$⊢Ⅎxy\in C$$
7	6	r19.36vf	$$⊢\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)$$
8	5 7	syl	$$⊢\exists x\in AB\subseteq C\to \left(\forall x\in Ay\in B\to y\in C\right)$$
9	3 8	biimtrid	$$⊢\exists x\in AB\subseteq C\to \left(y\in \bigcap _{x\in A}B\to y\in C\right)$$
10	9	ssrdv	$$⊢\exists x\in AB\subseteq C\to \bigcap _{x\in A}B\subseteq C$$