Definition df-iin 4953

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4952. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4990. Theorem intiin 5017 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 4951	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1568	. . . . 5 class 𝑦
7	6, 3	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3076	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2738	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1569	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is used by:  eliin  4955  iineq1  4968  iineq2  4971  nfiin  4982  nfiing  4984  nfii1  4986  dfiin2g  4988  cbviin  4993  cbviing  4995  cbviinv  4997  intiin  5017  0iin  5021  viin  5022  iinxsng  5047  iinxprg  5048  iinuni  5057  iinabrex  33163  iineq1i  36985  iineq12i  36986  cbviinvw2  37022  cbviindavw  37052  cbviindavw2  37076  iineq12f  39097  iineq12dv  46121