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		eleq1w	|- ( y = w -> ( y e. C <-> w e. C ) )
2	1	ralbidv	|- ( y = w -> ( A. x e. B y e. C <-> A. x e. B w e. C ) )
3		eleq1	|- ( w = A -> ( w e. C <-> A e. C ) )
4	3	ralbidv	|- ( w = A -> ( A. x e. B w e. C <-> A. x e. B A e. C ) )
5		df-iin	|- |^|_ x e. B C = { y | A. x e. B y e. C }
6	2 4 5	elab2gw	|- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )