Definition df-in 3872

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 27892). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3870) and difference (𝐴 ∖ 𝐵) (df-dif 3868). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4163 and dfin4 4170. For intersection defined in terms of union, see dfin3 4169. (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 3864	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1524	. . . . 5 class 𝑥
6	5, 1	wcel 2083	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2083	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 396	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2777	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1525	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3873  dfss2  3883  elin  4096  disj  4319  iinxprg  4916  disjex  30028  disjexc  30029  eulerpartlemt  31242  iocinico  39324  csbingVD  40778