Theorem ssiinf

Description: Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012) (Proof shortened by Mario Carneiro, 14-Oct-2016)

	Ref	Expression
Hypothesis	ssiinf.1	|- F/_ x C
Assertion	ssiinf	|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )

Proof

Step	Hyp	Ref	Expression
1		ssiinf.1	|- F/_ x C
2		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
3	2	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
4	3	ralbii	|- ( A. y e. C y e. |^|_ x e. A B <-> A. y e. C A. x e. A y e. B )
5		nfcv	|- F/_ y A
6	1 5	ralcomf	|- ( A. y e. C A. x e. A y e. B <-> A. x e. A A. y e. C y e. B )
7	4 6	bitri	|- ( A. y e. C y e. |^|_ x e. A B <-> A. x e. A A. y e. C y e. B )
8		dfss3	|- ( C C_ |^|_ x e. A B <-> A. y e. C y e. |^|_ x e. A B )
9		dfss3	|- ( C C_ B <-> A. y e. C y e. B )
10	9	ralbii	|- ( A. x e. A C C_ B <-> A. x e. A A. y e. C y e. B )
11	7 8 10	3bitr4i	|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )