Definition df-iin 4961

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

Assertion

Ref	Expression
df-iin	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-iin

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	ciin 4959	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2109	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3045	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2708	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  4963  iineq1  4976  iineq2  4979  nfiin  4991  nfiing  4993  nfii1  4996  dfiin2g  4999  cbviin  5004  cbviing  5006  cbviinv  5008  intiin  5026  0iin  5031  viin  5032  iinxsng  5055  iinxprg  5056  iinuni  5065  iinabrex  32505  iineq1i  36191  iineq12i  36192  cbviinvw2  36228  cbviindavw  36258  cbviindavw2  36282  iineq12f  38165  iineq12dv  45107