Definition df-iin 4958

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

This definition is referenced by:  eliin  4960  iineq1  4973  iineq2  4976  nfiin  4988  nfiing  4990  nfii1  4992  dfiin2g  4994  cbviin  4999  cbviing  5001  cbviinv  5003  intiin  5023  0iin  5027  viin  5028  iinxsng  5053  iinxprg  5054  iinuni  5063  iinabrex  32880  iineq1i  36652  iineq12i  36653  cbviinvw2  36689  cbviindavw  36719  cbviindavw2  36743  iineq12f  38759  iineq12dv  45772