Definition df-iin

Description: Define indexed intersection. Definition of Stoll p. 45. See the remarks for its sibling operation of indexed union df-iun . An alternate definition tying indexed intersection to ordinary intersection is dfiin2 . Theorem intiin provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998)

	Ref	Expression
Assertion	df-iin	$$⊢\bigcap _{x\in A}B=\left\{y|\forall x\in Ay\in B\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	ciin	$$class\bigcap _{x\in A}B$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 2	wcel	$$wffy\in B$$
7	6 0 1	wral	$$wff\forall x\in Ay\in B$$
8	7 4	cab	$$class\left\{y|\forall x\in Ay\in B\right\}$$
9	3 8	wceq	$$wff\bigcap _{x\in A}B=\left\{y|\forall x\in Ay\in B\right\}$$