Theorem iinss1

Description: Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		ssralv	|- ( A C_ B -> ( A. x e. B y e. C -> A. x e. A y e. C ) )
2		eliin	|- ( y e. _V -> ( y e. |^|_ x e. B C <-> A. x e. B y e. C ) )
3	2	elv	|- ( y e. |^|_ x e. B C <-> A. x e. B y e. C )
4		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
5	4	elv	|- ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
6	1 3 5	3imtr4g	|- ( A C_ B -> ( y e. |^|_ x e. B C -> y e. |^|_ x e. A C ) )
7	6	ssrdv	|- ( A C_ B -> |^|_ x e. B C C_ |^|_ x e. A C )