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	|- |^|_ x e. A B = { y | A. x e. A y e. B }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		cA	|- A
2		cB	|- B
3	0 1 2	ciin	|- |^|_ x e. A B
4		vy	|- y
5	4	cv	|- y
6	5 2	wcel	|- y e. B
7	6 0 1	wral	|- A. x e. A y e. B
8	7 4	cab	|- { y | A. x e. A y e. B }
9	3 8	wceq	|- |^|_ x e. A B = { y | A. x e. A y e. B }