Definition df-iin 4936

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

This definition is referenced by:  eliin  4938  iineq1  4951  iineq2  4954  nfiin  4966  nfiing  4968  nfii1  4971  dfiin2g  4973  cbviin  4978  cbviing  4980  cbviinv  4982  intiin  5002  0iin  5006  viin  5007  iinxsng  5030  iinxprg  5031  iinuni  5040  iinabrex  32639  iineq1i  36378  iineq12i  36379  cbviinvw2  36415  cbviindavw  36445  cbviindavw2  36469  iineq12f  38485  iineq12dv  45536