Theorem iinab

Description: Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011)

	Ref	Expression
Assertion	iinab	$$⊢\bigcap _{x\in A}\left\{y|\phi \right\}=\left\{y|\forall x\in A\phi \right\}$$

Proof

Step	Hyp	Ref	Expression
1		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
2		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\phi \right\}$$
3	1 2	nfiin	$$⊢\underset{\_}{Ⅎ}y\bigcap _{x\in A}\left\{y|\phi \right\}$$
4		nfab1	$$⊢\underset{\_}{Ⅎ}y\left\{y|\forall x\in A\phi \right\}$$
5		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
6	5	ralbii	$$⊢\forall x\in Ay\in \left\{y|\phi \right\}\leftrightarrow \forall x\in A\phi$$
7		eliin	$$⊢y\in \mathrm{V}\to \left(y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow \forall x\in Ay\in \left\{y|\phi \right\}\right)$$
8	7	elv	$$⊢y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow \forall x\in Ay\in \left\{y|\phi \right\}$$
9		abid	$$⊢y\in \left\{y|\forall x\in A\phi \right\}\leftrightarrow \forall x\in A\phi$$
10	6 8 9	3bitr4i	$$⊢y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\forall x\in A\phi \right\}$$
11	3 4 10	eqri	$$⊢\bigcap _{x\in A}\left\{y|\phi \right\}=\left\{y|\forall x\in A\phi \right\}$$