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 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2145	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3076	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2738	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	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  33096  iineq1i  36907  iineq12i  36908  cbviinvw2  36944  cbviindavw  36974  cbviindavw2  36998  iineq12f  39016  iineq12dv  46042