Theorem iinss2d

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		iinss2d.1	|- F/ x ph
2		iinss2d.2	|- F/_ x A
3		iinss2d.3	|- F/_ x C
4		iinss2d.4	|- ( ph -> A =/= (/) )
5		iinss2d.5	|- ( ( ph /\ x e. A ) -> B C_ C )
6	5	3adant3	|- ( ( ph /\ x e. A /\ T. ) -> B C_ C )
7	2	n0f	|- ( A =/= (/) <-> E. x x e. A )
8	4 7	sylib	|- ( ph -> E. x x e. A )
9		rextru	|- ( E. x x e. A <-> E. x e. A T. )
10	8 9	sylib	|- ( ph -> E. x e. A T. )
11	1 6 10	reximdd	|- ( 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 )