Definition df-iin 4957

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

This definition is used by:  eliin  4959  iineq1  4972  iineq2  4975  nfiin  4986  nfiing  4988  nfii1  4990  dfiin2g  4992  cbviin  4997  cbviing  4999  cbviinv  5001  intiin  5021  0iin  5025  viin  5026  iinxsng  5051  iinxprg  5052  iinuni  5061  iinabrex  33232  iineq1i  37162  iineq12i  37163  cbviinvw2  37199  cbviindavw  37229  cbviindavw2  37253  iineq12f  39287  iineq12dv  46324