Definition df-in 2103

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 2296 and dfin4 2300. For intersection defined in terms of union, see dfin3 2299.

Assertion

Ref	Expression
df-in	|- (A i^i B) = {x | (x e. A /\ x e. B)}

Distinct variable groups:   x,A   x,B

Detailed syntax breakdown of Definition df-in

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cin 2098	. 2 class (A i^i B)
4		vx	. . . . . 6 set x
5	4	cv 991	. . . . 5 class x
6	5, 1	wcel 994	. . . 4 wff x e. A
7	5, 2	wcel 994	. . . 4 wff x e. B
8	6, 7	wa 221	. . 3 wff (x e. A /\ x e. B)
9	8, 4	cab 1505	. 2 class {x | (x e. A /\ x e. B)}
10	3, 9	wceq 992	1 wff (A i^i B) = {x | (x e. A /\ x e. B)}

This definition is referenced by:  dfin5 2104  dfss2 2110  elin 2259  disj 2364

Copyright terms: Public domain