Definition df-iin 4970

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4969. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5010. Theorem intiin 5035 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 4968	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3051	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2713	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  4972  iineq1  4985  iineq2  4988  nfiin  5000  nfiing  5002  nfii1  5005  dfiin2g  5008  cbviin  5013  cbviing  5015  cbviinv  5017  intiin  5035  0iin  5040  viin  5041  iinxsng  5064  iinxprg  5065  iinuni  5074  iinabrex  32496  iineq1i  36160  iineq12i  36161  cbviinvw2  36197  cbviindavw  36227  cbviindavw2  36251  iineq12f  38134  iineq12dv  45078