Definition df-iin 4944

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

This definition is referenced by:  eliin  4946  iineq1  4959  iineq2  4962  nfiin  4974  nfiing  4976  nfii1  4979  dfiin2g  4981  cbviin  4986  cbviing  4988  cbviinv  4990  intiin  5008  0iin  5012  viin  5013  iinxsng  5036  iinxprg  5037  iinuni  5046  iinabrex  32544  iineq1i  36229  iineq12i  36230  cbviinvw2  36266  cbviindavw  36296  cbviindavw2  36320  iineq12f  38203  iineq12dv  45142