Definition df-int 4011

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

Assertion

Ref	Expression
df-int	|- |^| A = { x | A. y ( y e. A -> x e. 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 4010	. 2 class |^| A
3		vy	. . . . . . 7 set y
4	3	cv 1648	. . . . . 6 class y
5	4, 1	wcel 1721	. . . . 5 wff y e. A
6		vx	. . . . . 6 set x
7	6, 3	wel 1722	. . . . 5 wff x e. y
8	5, 7	wi 4	. . . 4 wff ( y e. A -> x e. y )
9	8, 3	wal 1546	. . 3 wff A. y ( y e. A -> x e. y )
10	9, 6	cab 2390	. 2 class { x | A. y ( y e. A -> x e. y ) }
11	2, 10	wceq 1649	1 wff |^| A = { x | A. y ( y e. A -> x e. y ) }

This definition is referenced by:  dfint2  4012  elint  4016  int0  4024  dfiin2g  4084