Definition df-in 3933

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30352). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3931) and difference (𝐴 ∖ 𝐵) (df-dif 3929). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4246 and dfin4 4253. For intersection defined in terms of union, see dfin3 4252. (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 3925	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1539	. . . . 5 class 𝑥
6	5, 1	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2108	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2713	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1540	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3934  elin  3942  dfss2  3944  disj  4425  iinxprg  5065  disjex  32519  disjexc  32520  eulerpartlemt  34349  in-ax8  36188  iocinico  43183  csbingVD  44856