Definition df-in 3906

Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 30416). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3904) and difference (𝐴 ∖ 𝐵) (df-dif 3902). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4222 and dfin4 4229. For intersection defined in terms of union, see dfin3 4228. (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 3898	. 2 class (𝐴 ∩ 𝐵)
4		vx	. . . . . 6 setvar 𝑥
5	4	cv 1540	. . . . 5 class 𝑥
6	5, 1	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐴
7	5, 2	wcel 2113	. . . 4 wff 𝑥 ∈ 𝐵
8	6, 7	wa 395	. . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)
9	8, 4	cab 2711	. 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}
10	3, 9	wceq 1541	1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)}

This definition is referenced by:  dfin5  3907  elin  3915  dfss2  3917  disj  4401  iinxprg  5041  disjex  32583  disjexc  32584  eulerpartlemt  34395  in-ax8  36279  iocinico  43319  csbingVD  44990