Theorem iinrab2

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

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

Proof

Step	Hyp	Ref	Expression
1		iineq1	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}=\bigcap _{x\in \varnothing }\left\{y\in B|\phi \right\}$$
2		0iin	$$⊢\bigcap _{x\in \varnothing }\left\{y\in B|\phi \right\}=\mathrm{V}$$
3	1 2	eqtrdi	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}=\mathrm{V}$$
4	3	ineq1d	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\mathrm{V}\cap B$$
5		incom	$$⊢\mathrm{V}\cap B=B\cap \mathrm{V}$$
6		inv1	$$⊢B\cap \mathrm{V}=B$$
7	5 6	eqtri	$$⊢\mathrm{V}\cap B=B$$
8	4 7	eqtrdi	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=B$$
9		rzal	$$⊢A=\varnothing \to \forall x\in A\forall y\in B\phi$$
10		rabid2	$$⊢B=\left\{y\in B|\forall x\in A\phi \right\}\leftrightarrow \forall y\in B\forall x\in A\phi$$
11		ralcom	$$⊢\forall y\in B\forall x\in A\phi \leftrightarrow \forall x\in A\forall y\in B\phi$$
12	10 11	bitr2i	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow B=\left\{y\in B|\forall x\in A\phi \right\}$$
13	9 12	sylib	$$⊢A=\varnothing \to B=\left\{y\in B|\forall x\in A\phi \right\}$$
14	8 13	eqtrd	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\left\{y\in B|\forall x\in A\phi \right\}$$
15		iinrab	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}=\left\{y\in B|\forall x\in A\phi \right\}$$
16	15	ineq1d	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\left\{y\in B|\forall x\in A\phi \right\}\cap B$$
17		ssrab2	$$⊢\left\{y\in B|\forall x\in A\phi \right\}\subseteq B$$
18		dfss	$$⊢\left\{y\in B|\forall x\in A\phi \right\}\subseteq B\leftrightarrow \left\{y\in B|\forall x\in A\phi \right\}=\left\{y\in B|\forall x\in A\phi \right\}\cap B$$
19	17 18	mpbi	$$⊢\left\{y\in B|\forall x\in A\phi \right\}=\left\{y\in B|\forall x\in A\phi \right\}\cap B$$
20	16 19	eqtr4di	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\left\{y\in B|\forall x\in A\phi \right\}$$
21	14 20	pm2.61ine	$$⊢\bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\left\{y\in B|\forall x\in A\phi \right\}$$