Definition df-in 3943

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 28204). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3941) and difference (𝐴 ∖ 𝐵) (df-dif 3939). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4237 and dfin4 4244. For intersection defined in terms of union, see dfin3 4243. (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 3935	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1536	. . . . 5 class 𝑥
6	5, 1	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2114	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 398	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2799	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1537	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3944  dfss2  3955  elin  4169  disj  4399  iinxprg  5011  disjex  30342  disjexc  30343  eulerpartlemt  31629  iocinico  39867  csbingVD  41267