Definition df-iin 4998

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4997. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5038. Theorem intiin 5063 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 4996	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1535	. . . . 5 class 𝑦
7	6, 3	wcel 2105	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3058	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2711	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1536	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  5000  iineq1  5013  iineq2  5016  nfiin  5028  nfiing  5030  nfii1  5033  dfiin2g  5036  cbviin  5041  cbviing  5043  cbviinv  5045  intiin  5063  0iin  5068  viin  5069  iinxsng  5092  iinxprg  5093  iinuni  5102  iinabrex  32588  iineq1i  36177  iineq12i  36178  cbviinvw2  36215  cbviindavw  36245  cbviindavw2  36269  iineq12f  38150  iineq12dv  45045