Definition df-iin 4926

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4925. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4964. Theorem intiin 4991 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 4924	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1547	. . . . 5 class 𝑦
7	6, 3	wcel 2121	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3055	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2719	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1548	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  4928  iineq1  4941  iineq2  4944  nfiin  4956  nfiing  4958  nfii1  4960  dfiin2g  4962  cbviin  4967  cbviing  4969  cbviinv  4971  intiin  4991  0iin  4995  viin  4996  iinxsng  5019  iinxprg  5020  iinuni  5029  iinabrex  32660  iineq1i  36437  iineq12i  36438  cbviinvw2  36474  cbviindavw  36504  cbviindavw2  36528  iineq12f  38544  iineq12dv  45565