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		inv1	$$⊢B\cap \mathrm{V}=B$$
6	5	ineqcomi	$$⊢\mathrm{V}\cap B=B$$
7	4 6	eqtrdi	$$⊢A=\varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=B$$
8		rzal	$$⊢A=\varnothing \to \forall x\in A\forall y\in B\phi$$
9		rabid2	$$⊢B=\left\{y\in B|\forall x\in A\phi \right\}\leftrightarrow \forall y\in B\forall x\in A\phi$$
10		ralcom	$$⊢\forall y\in B\forall x\in A\phi \leftrightarrow \forall x\in A\forall y\in B\phi$$
11	9 10	bitr2i	$$⊢\forall x\in A\forall y\in B\phi \leftrightarrow B=\left\{y\in B|\forall x\in A\phi \right\}$$
12	8 11	sylib	$$⊢A=\varnothing \to B=\left\{y\in B|\forall x\in A\phi \right\}$$
13	7 12	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\}$$
14		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\}$$
15	14	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$$
16		ssrab2	$$⊢\left\{y\in B|\forall x\in A\phi \right\}\subseteq B$$
17		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$$
18	16 17	mpbi	$$⊢\left\{y\in B|\forall x\in A\phi \right\}=\left\{y\in B|\forall x\in A\phi \right\}\cap B$$
19	15 18	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\}$$
20	13 19	pm2.61ine	$$⊢\bigcap _{x\in A}\left\{y\in B|\phi \right\}\cap B=\left\{y\in B|\forall x\in A\phi \right\}$$