Definition df-iin 5018

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 5017. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 5057. Theorem intiin 5082 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 5016	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1536	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3067	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2717	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1537	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  5020  iineq1  5032  iineq2  5035  nfiin  5047  nfiing  5049  nfii1  5052  dfiin2g  5055  cbviin  5060  cbviing  5062  cbviinv  5064  intiin  5082  0iin  5087  viin  5088  iinxsng  5111  iinxprg  5112  iinuni  5121  iinabrex  32591  iineq1i  36160  iineq12i  36161  cbviinvw2  36199  cbviindavw  36229  cbviindavw2  36253  iineq12f  38124  iineq12dv  45008