Theorem iinrab

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

	Ref	Expression
Assertion	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\}$$

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	$$⊢A\ne \varnothing \to \left(\forall x\in A\left(y\in B\wedge \phi \right)\leftrightarrow \left(y\in B\wedge \forall x\in A\phi \right)\right)$$
2	1	abbidv	$$⊢A\ne \varnothing \to \left\{y|\forall x\in A\left(y\in B\wedge \phi \right)\right\}=\left\{y|\left(y\in B\wedge \forall x\in A\phi \right)\right\}$$
3		df-rab	$$⊢\left\{y\in B|\phi \right\}=\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
4	3	a1i	$$⊢x\in A\to \left\{y\in B|\phi \right\}=\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
5	4	iineq2i	$$⊢\bigcap _{x\in A}\left\{y\in B|\phi \right\}=\bigcap _{x\in A}\left\{y|\left(y\in B\wedge \phi \right)\right\}$$
6		iinab	$$⊢\bigcap _{x\in A}\left\{y|\left(y\in B\wedge \phi \right)\right\}=\left\{y|\forall x\in A\left(y\in B\wedge \phi \right)\right\}$$
7	5 6	eqtri	$$⊢\bigcap _{x\in A}\left\{y\in B|\phi \right\}=\left\{y|\forall x\in A\left(y\in B\wedge \phi \right)\right\}$$
8		df-rab	$$⊢\left\{y\in B|\forall x\in A\phi \right\}=\left\{y|\left(y\in B\wedge \forall x\in A\phi \right)\right\}$$
9	2 7 8	3eqtr4g	$$⊢A\ne \varnothing \to \bigcap _{x\in A}\left\{y\in B|\phi \right\}=\left\{y\in B|\forall x\in A\phi \right\}$$