![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > df-in | Structured version Visualization version GIF version |
Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 27892). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3870) and difference (𝐴 ∖ 𝐵) (df-dif 3868). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4163 and dfin4 4170. For intersection defined in terms of union, see dfin3 4169. (Contributed by NM, 29-Apr-1994.) |
Ref | Expression |
---|---|
df-in | ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | cB | . . 3 class 𝐵 | |
3 | 1, 2 | cin 3864 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1524 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2083 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2083 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2777 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1525 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3873 dfss2 3883 elin 4096 disj 4319 iinxprg 4916 disjex 30028 disjexc 30029 eulerpartlemt 31242 iocinico 39324 csbingVD 40778 |
Copyright terms: Public domain | W3C validator |