Theorem eliin

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

	Ref	Expression
Assertion	eliin	$$⊢A\in V\to \left(A\in \bigcap _{x\in B}C\leftrightarrow \forall x\in BA\in C\right)$$

Proof

Step	Hyp	Ref	Expression
1		eleq1	$$⊢y=A\to \left(y\in C\leftrightarrow A\in C\right)$$
2	1	ralbidv	$$⊢y=A\to \left(\forall x\in By\in C\leftrightarrow \forall x\in BA\in C\right)$$
3		df-iin	$$⊢\bigcap _{x\in B}C=\left\{y|\forall x\in By\in C\right\}$$
4	2 3	elab2g	$$⊢A\in V\to \left(A\in \bigcap _{x\in B}C\leftrightarrow \forall x\in BA\in C\right)$$