Definition df-iin 4958

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

This definition is used by:  eliin  4960  iineq1  4973  iineq2  4976  nfiin  4988  nfiing  4990  nfii1  4992  dfiin2g  4994  cbviin  4999  cbviing  5001  cbviinv  5003  intiin  5023  0iin  5027  viin  5028  iinxsng  5053  iinxprg  5054  iinuni  5063  iinabrex  32925  iineq1i  36736  iineq12i  36737  cbviinvw2  36773  cbviindavw  36803  cbviindavw2  36827  iineq12f  38841  iineq12dv  45852