Definition df-int 1966

Description: Define the intersection of a class. Definition 7.35 of [TakeutiZaring] p. 44.

Assertion

Ref	Expression
df-int	|- |^|A = {x | A.y(y e. A -> x e. y)}

Distinct variable group(s):   x,y,A

Detailed syntax breakdown of Definition df-int

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	cint 1965	. 2 class |^|A
3		vy	. . . . . . 7 set y
4	3	cv 1089	. . . . . 6 class y
5	4, 1	wcel 1092	. . . . 5 wff y e. A
6		vx	. . . . . 6 set x
7	6, 3	wel 803	. . . . 5 wff x e. y
8	5, 7	wi 2	. . . 4 wff (y e. A -> x e. y)
9	8, 3	wal 672	. . 3 wff A.y(y e. A -> x e. y)
10	9, 6	cab 1090	. 2 class {x | A.y(y e. A -> x e. y)}
11	2, 10	wceq 1091	1 wff |^|A = {x | A.y(y e. A -> x e. y)}

This definition is referenced by:  dfint2 1967  elint 1971  int0 1978  dfiin2 2015

metamath.org