This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ∩ 𝑥 ∈ 𝐴 𝐵 = { 𝑦 ∣ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 }