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 4995. Theorem intiin 5022 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 2145	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3078	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2740	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is used by:  eliin  4959  iineq1  4972  iineq2  4975  nfiin  4987  nfiing  4989  nfii1  4991  dfiin2g  4993  cbviin  4998  cbviing  5000  cbviinv  5002  intiin  5022  0iin  5026  viin  5027  iinxsng  5052  iinxprg  5053  iinuni  5062  iinabrex  33029  iineq1i  36803  iineq12i  36804  cbviinvw2  36840  cbviindavw  36870  cbviindavw2  36894  iineq12f  38899  iineq12dv  45925