Definition df-in 3546

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 26467). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3544) and difference (𝐴 ∖ 𝐵) (df-dif 3542). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3821 and dfin4 3825. For intersection defined in terms of union, see dfin3 3824. (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 3538	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1473	. . . . 5 class 𝑥
6	5, 1	wcel 1976	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 1976	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 382	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2595	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1474	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3547  dfss2  3556  elin  3757  disj  3968  iinxprg  4531  disjex  28580  disjexc  28581  eulerpartlemt  29553  iocinico  36599  csbingVD  37925