Definition df-iin 5001

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 5000. 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 4999	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3062	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2710	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  5003  iineq1  5015  iineq2  5018  nfiin  5029  nfiing  5031  nfii1  5033  dfiin2g  5036  cbviin  5041  cbviing  5043  intiin  5063  0iin  5068  viin  5069  iinxsng  5092  iinxprg  5093  iinuni  5102  iinabrex  31800  iineq12f  37032