Definition df-in 3915

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

This definition is used by:  dfin5  3916  elin  3924  dfss2  3926  disj  4413  iinxprg  5060  disjex  32967  disjexc  32968  eulerpartlemt  34785  in-ax8  36769  iocinico  43972  csbingVD  45625