Definition df-in 3567

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 27170). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3565) and difference (𝐴 ∖ 𝐵) (df-dif 3563). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3844 and dfin4 3849. For intersection defined in terms of union, see dfin3 3848. (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 3559	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1479	. . . . 5 class 𝑥
6	5, 1	wcel 1987	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 1987	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 384	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2607	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1480	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3568  dfss2  3577  elin  3780  disj  3995  iinxprg  4574  disjex  29291  disjexc  29292  eulerpartlemt  30256  iocinico  37317  csbingVD  38642