Definition df-iin 4954

Description: Define indexed intersection. Definition of [Stoll] p. 45. See the remarks for its sibling operation of indexed union df-iun 4953. An alternate definition tying indexed intersection to ordinary intersection is dfiin2 4992. Theorem intiin 5019 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 4952	. 2 class ∩ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1561	. . . . 5 class 𝑦
7	6, 3	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wral 3078	. . 3 wff ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2742	. 2 class {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1562	1 wff ∩ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliin  4956  iineq1  4969  iineq2  4972  nfiin  4984  nfiing  4986  nfii1  4988  dfiin2g  4990  cbviin  4995  cbviing  4997  cbviinv  4999  intiin  5019  0iin  5023  viin  5024  iinxsng  5047  iinxprg  5048  iinuni  5057  iinabrex  32771  iineq1i  36561  iineq12i  36562  cbviinvw2  36598  cbviindavw  36628  cbviindavw2  36652  iineq12f  38668  iineq12dv  45689