Definition df-int 3927

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 3213. (Contributed by NM, 18-Aug-1993.)

Assertion

Ref	Expression
df-int	⊢ ∩A = {x ∣ ∀y(y ∈ A → x ∈ y)}

Distinct variable group:   x,y,A

Detailed syntax breakdown of Definition df-int

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cint 3926	. 2 class ∩A
3		vy	. . . . . . 7 setvar y
4	3	cv 1641	. . . . . 6 class y
5	4, 1	wcel 1710	. . . . 5 wff y ∈ A
6		vx	. . . . . 6 setvar x
7	6, 3	wel 1711	. . . . 5 wff x ∈ y
8	5, 7	wi 4	. . . 4 wff (y ∈ A → x ∈ y)
9	8, 3	wal 1540	. . 3 wff ∀y(y ∈ A → x ∈ y)
10	9, 6	cab 2339	. 2 class {x ∣ ∀y(y ∈ A → x ∈ y)}
11	2, 10	wceq 1642	1 wff ∩A = {x ∣ ∀y(y ∈ A → x ∈ y)}

This definition is referenced by:  dfint2  3928  elint  3932  int0  3940  dfiin2g  4000