Definition df-in 3909

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

This definition is used by:  dfin5  3910  elin  3918  dfss2  3920  disj  4406  iinxprg  5053  disjex  33073  disjexc  33074  eulerpartlemt  34890  in-ax8  36852  iocinico  44061  csbingVD  45714