Definition df-in 3955

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 29668). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3953) and difference (𝐴 ∖ 𝐵) (df-dif 3951). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4260 and dfin4 4267. For intersection defined in terms of union, see dfin3 4266. (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 3947	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1541	. . . . 5 class 𝑥
6	5, 1	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2107	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 397	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2710	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1542	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3956  elin  3964  dfss2OLD  3969  ss2abdv  4060  disj  4447  disjOLD  4448  iinxprg  5092  disjex  31811  disjexc  31812  eulerpartlemt  33359  iocinico  41947  csbingVD  43631