Theorem eliin

Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003)

	Ref	Expression
Assertion	eliin	|- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( y = A -> ( y e. C <-> A e. C ) )
2	1	ralbidv	|- ( y = A -> ( A. x e. B y e. C <-> A. x e. B A e. C ) )
3		df-iin	|- |^|_ x e. B C = { y | A. x e. B y e. C }
4	2 3	elab2g	|- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )