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 | A. y ( y e. A -> x e. y ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	|- A
1	0	cint	|- |^| A
2		vx	|- x
3		vy	|- y
4	3	cv	|- y
5	4 0	wcel	|- y e. A
6	2	cv	|- x
7	6 4	wcel	|- x e. y
8	5 7	wi	|- ( y e. A -> x e. y )
9	8 3	wal	|- A. y ( y e. A -> x e. y )
10	9 2	cab	|- { x | A. y ( y e. A -> x e. y ) }
11	1 10	wceq	|- |^| A = { x | A. y ( y e. A -> x e. y ) }