Definition df-in 3969

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30453). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3967) and difference (𝐴 ∖ 𝐵) (df-dif 3965). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4276 and dfin4 4283. For intersection defined in terms of union, see dfin3 4282. (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 3961	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1535	. . . . 5 class 𝑥
6	5, 1	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2105	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2711	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1536	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3970  elin  3978  dfss2  3980  disj  4455  iinxprg  5093  disjex  32611  disjexc  32612  eulerpartlemt  34352  in-ax8  36206  iocinico  43200  csbingVD  44881