Definition df-in 3907

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

This definition is referenced by:  dfin5  3908  elin  3916  dfss2  3918  disj  4398  iinxprg  5035  disjex  32562  disjexc  32563  eulerpartlemt  34374  in-ax8  36237  iocinico  43224  csbingVD  44895