Definition df-in 3938

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

This definition is referenced by:  dfin5  3939  elin  3947  dfss2  3949  disj  4430  iinxprg  5069  disjex  32541  disjexc  32542  eulerpartlemt  34348  in-ax8  36200  iocinico  43202  csbingVD  44876