Theorem iinssf

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

	Ref	Expression
Hypothesis	iinssf.1	|- F/_ x C
Assertion	iinssf	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		iinssf.1	|- F/_ x C
2		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
3	2	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
4		ssel	|- ( B C_ C -> ( y e. B -> y e. C ) )
5	4	reximi	|- ( E. x e. A B C_ C -> E. x e. A ( y e. B -> y e. C ) )
6	1	nfcri	|- F/ x y e. C
7	6	r19.36vf	|- ( E. x e. A ( y e. B -> y e. C ) -> ( A. x e. A y e. B -> y e. C ) )
8	5 7	syl	|- ( E. x e. A B C_ C -> ( A. x e. A y e. B -> y e. C ) )
9	3 8	biimtrid	|- ( E. x e. A B C_ C -> ( y e. |^|_ x e. A B -> y e. C ) )
10	9	ssrdv	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )