Definition df-in 3581

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 27282). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3579) and difference (𝐴 ∖ 𝐵) (df-dif 3577). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3860 and dfin4 3867. For intersection defined in terms of union, see dfin3 3866. (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 3573	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1482	. . . . 5 class 𝑥
6	5, 1	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 1990	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2608	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1483	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3582  dfss2  3591  elin  3796  disj  4017  iinxprg  4601  disjex  29405  disjexc  29406  eulerpartlemt  30433  iocinico  37797  csbingVD  39120