Theorem iinssd

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

	Ref	Expression
Hypotheses	iinssd.1	|- ( ph -> X e. A )
	iinssd.2	|- ( x = X -> B = D )
	iinssd.3	|- ( ph -> D C_ C )
Assertion	iinssd	|- ( ph -> |^|_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		iinssd.1	|- ( ph -> X e. A )
2		iinssd.2	|- ( x = X -> B = D )
3		iinssd.3	|- ( ph -> D C_ C )
4	2	sseq1d	|- ( x = X -> ( B C_ C <-> D C_ C ) )
5	4	rspcev	|- ( ( X e. A /\ D C_ C ) -> E. x e. A B C_ C )
6	1 3 5	syl2anc	|- ( ph -> E. x e. A B C_ C )
7		iinss	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
8	6 7	syl	|- ( ph -> |^|_ x e. A B C_ C )