Definition df-in 1491

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 1669 and dfin4 1673. For intersection defined in terms of union, see dfin3 1672.

Assertion

Ref	Expression
df-in	⊢ (A ∩ B) = {x∣(x ∈ A ∧ x ∈ B)}

Distinct variable group(s):   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 1486	. 2 class (A ∩ B)
4		vx	. . . . . 6 set x
5	4	cv 1089	. . . . 5 class x
6	5, 1	wcel 1092	. . . 4 wff x ∈ A
7	5, 2	wcel 1092	. . . 4 wff x ∈ B
8	6, 7	wa 196	. . 3 wff (x ∈ A ∧ x ∈ B)
9	8, 4	cab 1090	. 2 class {x∣(x ∈ A ∧ x ∈ B)}
10	3, 9	wceq 1091	1 wff (A ∩ B) = {x∣(x ∈ A ∧ x ∈ B)}

This definition is referenced by:  dfss2 1497  elin 1635  disj 1733

metamath.org