Theorem iinssdf

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

	Ref	Expression
Hypotheses	iinssdf.a	|- F/_ x A
	iinssdf.n	|- F/_ x X
	iinssdf.c	|- F/_ x C
	iinssdf.d	|- F/_ x D
	iinssdf.x	|- ( ph -> X e. A )
	iinssdf.b	|- ( x = X -> B = D )
	iinssdf.s	|- ( ph -> D C_ C )
Assertion	iinssdf	|- ( ph -> |^|_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		iinssdf.a	|- F/_ x A
2		iinssdf.n	|- F/_ x X
3		iinssdf.c	|- F/_ x C
4		iinssdf.d	|- F/_ x D
5		iinssdf.x	|- ( ph -> X e. A )
6		iinssdf.b	|- ( x = X -> B = D )
7		iinssdf.s	|- ( ph -> D C_ C )
8	4 3	nfss	|- F/ x D C_ C
9	6	sseq1d	|- ( x = X -> ( B C_ C <-> D C_ C ) )
10	8 2 1 9	rspcef	|- ( ( X e. A /\ D C_ C ) -> E. x e. A B C_ C )
11	5 7 10	syl2anc	|- ( ph -> E. x e. A B C_ C )
12	3	iinssf	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
13	11 12	syl	|- ( ph -> |^|_ x e. A B C_ C )