Definition df-iin 4927

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4926. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4965. Theorem intiin 4992 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 4925	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1547	. . . . 5 class 𝑦
7	6, 3	wcel 2121	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3055	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2719	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1548	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  4929  iineq1  4942  iineq2  4945  nfiin  4957  nfiing  4959  nfii1  4961  dfiin2g  4963  cbviin  4968  cbviing  4970  cbviinv  4972  intiin  4992  0iin  4996  viin  4997  iinxsng  5020  iinxprg  5021  iinuni  5030  iinabrex  32662  iineq1i  36439  iineq12i  36440  cbviinvw2  36476  cbviindavw  36506  cbviindavw2  36530  iineq12f  38546  iineq12dv  45567