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 ⊢ ⋂ x ∈ A B = y | ∀ x ∈ A y ∈ B

Detailed syntax breakdown

Step Hyp Ref Expression
0 vx setvar x
1 cA class A
2 cB class B
3 0 1 2 ciin class ⋂ x ∈ A B
4 vy setvar y
5 4 cv setvar y
6 5 2 wcel wff y ∈ B
7 6 0 1 wral wff ∀ x ∈ A y ∈ B
8 7 4 cab class y | ∀ x ∈ A y ∈ B
9 3 8 wceq wff ⋂ x ∈ A B = y | ∀ x ∈ A y ∈ B