Definition df-in 2041

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 2234 and dfin4 2238. For intersection defined in terms of union, see dfin3 2237.

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

This definition is referenced by:  dfin5 2042  dfss2 2048  elin 2197  disj 2301

Copyright terms: Public domain