Definition df-in 2603

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 2830 and dfin4 2835. For intersection defined in terms of union, see dfin3 2834.

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 2592	. 2 class (A i^i B)
4		vx	. . . . . 6 set x
5	4	cv 1297	. . . . 5 class x
6	5, 1	wcel 1300	. . . 4 wff x e. A
7	5, 2	wcel 1300	. . . 4 wff x e. B
8	6, 7	wa 240	. . 3 wff (x e. A /\ x e. B)
9	8, 4	cab 1871	. 2 class {x | (x e. A /\ x e. B)}
10	3, 9	wceq 1298	1 wff (A i^i B) = {x | (x e. A /\ x e. B)}

This definition is referenced by:  dfin5 2604  dfss2 2610  elin 2786  disj 2914  sbsslemOLD 2979

Copyright terms: Public domain