Definition df-in 3952

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30291). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3950) and difference (𝐴 ∖ 𝐵) (df-dif 3948). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4260 and dfin4 4267. For intersection defined in terms of union, see dfin3 4266. (Contributed by NM, 29-Apr-1994.)

Assertion

Ref	Expression
df-in	⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-in

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3	1, 2	cin 3944	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1532	. . . . 5 class 𝑥
6	5, 1	wcel 2098	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2098	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 394	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2702	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1533	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3953  elin  3961  dfss2  3963  disj  4448  disjOLD  4449  iinxprg  5092  disjex  32439  disjexc  32440  eulerpartlemt  34061  iocinico  42705  csbingVD  44388