Definition df-iin

Description: Define indexed intersection. Definition of Stoll p. 45. See the remarks for its sibling operation of indexed union df-iun . An alternate definition tying indexed intersection to ordinary intersection is dfiin2 . Theorem intiin provides a definition of ordinary intersection in terms of indexed intersection. (Contributed by NM, 27-Jun-1998)

	Ref	Expression
Assertion	df-iin	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	⊢ 𝑥
1		cA	⊢ 𝐴
2		cB	⊢ 𝐵
3	0 1 2	ciin	⊢ ∩ 𝑥 ∈ 𝐴 𝐵
4		vy	⊢ 𝑦
5	4	cv	⊢ 𝑦
6	5 2	wcel	⊢ 𝑦 ∈ 𝐵
7	6 0 1	wral	⊢ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
8	7 4	cab	⊢ { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }
9	3 8	wceq	⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }