Definition df-iin 3258

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 3257. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 3287. Theorem intiin 3307 provides a definition of ordinary intersection in terms of indexed intersection.

Assertion

Ref	Expression
df-iin	|- |^|_x e. A B = {y | A.x e. A y e. B}

Distinct variable groups:   x,y   y,A   y,B

Detailed syntax breakdown of Definition df-iin

Step	Hyp	Ref	Expression
1		vx	. . 3 set x
2		cA	. . 3 class A
3		cB	. . 3 class B
4	1, 2, 3	ciin 3256	. 2 class |^|_x e. A B
5		vy	. . . . . 6 set y
6	5	cv 1297	. . . . 5 class y
7	6, 3	wcel 1300	. . . 4 wff y e. B
8	7, 1, 2	wral 2105	. . 3 wff A.x e. A y e. B
9	8, 5	cab 1871	. 2 class {y | A.x e. A y e. B}
10	4, 9	wceq 1298	1 wff |^|_x e. A B = {y | A.x e. A y e. B}

This definition is referenced by:  eliin 3260  iineq1 3270  iineq2 3274  iineq2OLD 3275  hbii1 3282  dfiin2g 3286  dfiin2OLD 3288  intiin 3307  0iin 3313  viin 3314  iinab 3317  iin0 3477  dfiin2gOLD 15356  cbviin 15357  fclusss 15611

Copyright terms: Public domain