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 \| 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 ) }