Definition df-in 4094

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

This definition is used by:  dfin5  4095  elin  4096  dfss2  4097  disj  4406  iinxprg  5052  disjex  33258  disjexc  33259  eulerpartlemt  35073  in-ax8  37191  iocinico  44406  csbingVD  46057