Theorem iinss2

Description: An indexed intersection is included in any of its members. (Contributed by FL, 15-Oct-2012)

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

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		rsp	|- ( A. x e. A y e. B -> ( x e. A -> y e. B ) )
4	3	com12	|- ( x e. A -> ( A. x e. A y e. B -> y e. B ) )
5	2 4	syl5bi	|- ( x e. A -> ( y e. |^|_ x e. A B -> y e. B ) )
6	5	ssrdv	|- ( x e. A -> |^|_ x e. A B C_ B )