Theorem iinssiin

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

	Ref	Expression
Hypotheses	iinssiin.1	|- F/ x ph
	iinssiin.2	|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion	iinssiin	|- ( ph -> |^|_ x e. A B C_ |^|_ x e. A C )

Proof

Step	Hyp	Ref	Expression
1		iinssiin.1	|- F/ x ph
2		iinssiin.2	|- ( ( ph /\ x e. A ) -> B C_ C )
3		nfii1	|- F/_ x |^|_ x e. A B
4	3	nfcri	|- F/ x y e. |^|_ x e. A B
5	1 4	nfan	|- F/ x ( ph /\ y e. |^|_ x e. A B )
6	2	adantlr	|- ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> B C_ C )
7		eliinid	|- ( ( y e. |^|_ x e. A B /\ x e. A ) -> y e. B )
8	7	adantll	|- ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> y e. B )
9	6 8	sseldd	|- ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> y e. C )
10	9	ex	|- ( ( ph /\ y e. |^|_ x e. A B ) -> ( x e. A -> y e. C ) )
11	5 10	ralrimi	|- ( ( ph /\ y e. |^|_ x e. A B ) -> A. x e. A y e. C )
12		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
13	12	elv	|- ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
14	11 13	sylibr	|- ( ( ph /\ y e. |^|_ x e. A B ) -> y e. |^|_ x e. A C )
15	14	ssd	|- ( ph -> |^|_ x e. A B C_ |^|_ x e. A C )