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	3 4	cleqf	$$⊢\bigcap _{x\in A}\left\{y|\phi \right\}=\left\{y|\forall x\in A\phi \right\}\leftrightarrow \forall y\left(y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\forall x\in A\phi \right\}\right)$$
6		abid	$$⊢y\in \left\{y|\phi \right\}\leftrightarrow \phi$$
7	6	ralbii	$$⊢\forall x\in Ay\in \left\{y|\phi \right\}\leftrightarrow \forall x\in A\phi$$
8		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)$$
9	8	elv	$$⊢y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow \forall x\in Ay\in \left\{y|\phi \right\}$$
10		abid	$$⊢y\in \left\{y|\forall x\in A\phi \right\}\leftrightarrow \forall x\in A\phi$$
11	7 9 10	3bitr4i	$$⊢y\in \bigcap _{x\in A}\left\{y|\phi \right\}\leftrightarrow y\in \left\{y|\forall x\in A\phi \right\}$$
12	5 11	mpgbir	$$⊢\bigcap _{x\in A}\left\{y|\phi \right\}=\left\{y|\forall x\in A\phi \right\}$$