Definition df-in 2055

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 2248 and dfin4 2252. For intersection defined in terms of union, see dfin3 2251.

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 2050	. 2 class (A i^i B)
4		vx	. . . . . 6 set x
5	4	cv 957	. . . . 5 class x
6	5, 1	wcel 960	. . . 4 wff x e. A
7	5, 2	wcel 960	. . . 4 wff x e. B
8	6, 7	wa 223	. . 3 wff (x e. A /\ x e. B)
9	8, 4	cab 1466	. 2 class {x | (x e. A /\ x e. B)}
10	3, 9	wceq 958	1 wff (A i^i B) = {x | (x e. A /\ x e. B)}

This definition is referenced by:  dfin5 2056  dfss2 2062  elin 2211  disj 2316

Copyright terms: Public domain