Theorem iinss

Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	iinss	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
2	1	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
3		ssel	|- ( B C_ C -> ( y e. B -> y e. C ) )
4	3	reximi	|- ( E. x e. A B C_ C -> E. x e. A ( y e. B -> y e. C ) )
5		r19.36v	|- ( E. x e. A ( y e. B -> y e. C ) -> ( A. x e. A y e. B -> y e. C ) )
6	4 5	syl	|- ( E. x e. A B C_ C -> ( A. x e. A y e. B -> y e. C ) )
7	2 6	syl5bi	|- ( E. x e. A B C_ C -> ( y e. |^|_ x e. A B -> y e. C ) )
8	7	ssrdv	|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )