Theorem viin

Description: Indexed intersection with a universal index class. When A doesn't depend on x , this evaluates to A by 19.3 and abid2 . When A = x , this evaluates to (/) by intiin and intv . (Contributed by NM, 11-Sep-2008)

	Ref	Expression
Assertion	viin	$$⊢\bigcap _{x\in \mathrm{V}}A=\left\{y|\forall xy\in A\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-iin	$$⊢\bigcap _{x\in \mathrm{V}}A=\left\{y|\forall x\in \mathrm{V}y\in A\right\}$$
2		ralv	$$⊢\forall x\in \mathrm{V}y\in A\leftrightarrow \forall xy\in A$$
3	2	abbii	$$⊢\left\{y|\forall x\in \mathrm{V}y\in A\right\}=\left\{y|\forall xy\in A\right\}$$
4	1 3	eqtri	$$⊢\bigcap _{x\in \mathrm{V}}A=\left\{y|\forall xy\in A\right\}$$