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	$$⊢\bigcap A=\left\{x|\forall y\left(y\in A\to x\in y\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	cint	$$class\bigcap A$$
2		vx	$$setvarx$$
3		vy	$$setvary$$
4	3	cv	$$setvary$$
5	4 0	wcel	$$wffy\in A$$
6	2	cv	$$setvarx$$
7	6 4	wcel	$$wffx\in y$$
8	5 7	wi	$$wff\left(y\in A\to x\in y\right)$$
9	8 3	wal	$$wff\forall y\left(y\in A\to x\in y\right)$$
10	9 2	cab	$$class\left\{x|\forall y\left(y\in A\to x\in y\right)\right\}$$
11	1 10	wceq	$$wff\bigcap A=\left\{x|\forall y\left(y\in A\to x\in y\right)\right\}$$