Definition df-in 4091

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 31031). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 4151) and difference (𝐴 ∖ 𝐵) (df-dif 4047). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4216 and dfin4 4223. For intersection defined in terms of union, see dfin3 4222. (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 4089	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1568	. . . . 5 class 𝑥
6	5, 1	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2144	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 401	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2738	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1569	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is used by:  dfin5  4092  elin  4093  dfss2  4094  disj  4402  iinxprg  5048  disjex  33233  disjexc  33234  eulerpartlemt  35049  in-ax8  37105  iocinico  44307  csbingVD  45959