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

Metamath Proof Explorer

Definition df-int

Description: Define the intersection of a class. Definition 7.35 of TakeutiZaring p. 44. For example, |^| { { 1 , 3 } , { 1 , 8 } } = { 1 } . Compare this with the intersection of two classes, df-in . (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion df-int ⊢ ⋂ A = x | ∀ y y ∈ A → x ∈ y

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 cint class ⋂ A
2 vx setvar x
3 vy setvar y
4 3 cv setvar y
5 4 0 wcel wff y ∈ A
6 2 cv setvar x
7 6 4 wcel wff x ∈ y
8 5 7 wi wff y ∈ A → x ∈ y
9 8 3 wal wff ∀ y y ∈ A → x ∈ y
10 9 2 cab class x | ∀ y y ∈ A → x ∈ y
11 1 10 wceq wff ⋂ A = x | ∀ y y ∈ A → x ∈ y