Theorem riinrab

Description: Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		riin0	$$⊢X=\varnothing \to A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=A$$
2		rzal	$$⊢X=\varnothing \to \forall x\in X\phi$$
3	2	ralrimivw	$$⊢X=\varnothing \to \forall y\in A\forall x\in X\phi$$
4		rabid2	$$⊢A=\left\{y\in A|\forall x\in X\phi \right\}\leftrightarrow \forall y\in A\forall x\in X\phi$$
5	3 4	sylibr	$$⊢X=\varnothing \to A=\left\{y\in A|\forall x\in X\phi \right\}$$
6	1 5	eqtrd	$$⊢X=\varnothing \to A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\left\{y\in A|\forall x\in X\phi \right\}$$
7		ssrab2	$$⊢\left\{y\in A|\phi \right\}\subseteq A$$
8	7	rgenw	$$⊢\forall x\in X\left\{y\in A|\phi \right\}\subseteq A$$
9		riinn0	$$⊢\left(\forall x\in X\left\{y\in A|\phi \right\}\subseteq A\wedge X\ne \varnothing \right)\to A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\bigcap _{x\in X}\left\{y\in A|\phi \right\}$$
10	8 9	mpan	$$⊢X\ne \varnothing \to A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\bigcap _{x\in X}\left\{y\in A|\phi \right\}$$
11		iinrab	$$⊢X\ne \varnothing \to \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\left\{y\in A|\forall x\in X\phi \right\}$$
12	10 11	eqtrd	$$⊢X\ne \varnothing \to A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\left\{y\in A|\forall x\in X\phi \right\}$$
13	6 12	pm2.61ine	$$⊢A\cap \bigcap _{x\in X}\left\{y\in A|\phi \right\}=\left\{y\in A|\forall x\in X\phi \right\}$$