Definition df-in 2866

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 3072 and dfin4 3076. For intersection defined in terms of union, see dfin3 3075.

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 2858	. 2 class (A i^i B)
4		vx	. . . . . 6 set x
5	4	cv 1614	. . . . 5 class x
6	5, 1	wcel 1617	. . . 4 wff x e. A
7	5, 2	wcel 1617	. . . 4 wff x e. B
8	6, 7	wa 433	. . 3 wff (x e. A /\ x e. B)
9	8, 4	cab 2157	. 2 class {x | (x e. A /\ x e. B)}
10	3, 9	wceq 1615	1 wff (A i^i B) = {x | (x e. A /\ x e. B)}

This definition is referenced by:  dfin5 2867  dfss2 2873  elin 3031  disj 3150  csbingVD 17803

Copyright terms: Public domain