Definition df-in 3614

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 27412). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3612) and difference (𝐴 ∖ 𝐵) (df-dif 3610). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3893 and dfin4 3900. For intersection defined in terms of union, see dfin3 3899. (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 3606	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1522	. . . . 5 class 𝑥
6	5, 1	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2030	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 383	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2637	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1523	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3615  dfss2  3624  elin  3829  disj  4050  iinxprg  4633  disjex  29531  disjexc  29532  eulerpartlemt  30561  iocinico  38114  csbingVD  39434