| 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 30444). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3956) and difference (𝐴 ∖ 𝐵) (df-dif 3954). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4271 and dfin4 4278. For intersection defined in terms of union, see dfin3 4277. (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 3950 | . 2 class (𝐴 ∩ 𝐵) |
| 4 | vx | . . . . . 6 setvar 𝑥 | |
| 5 | 4 | cv 1539 | . . . . 5 class 𝑥 |
| 6 | 5, 1 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐴 |
| 7 | 5, 2 | wcel 2108 | . . . 4 wff 𝑥 ∈ 𝐵 |
| 8 | 6, 7 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
| 9 | 8, 4 | cab 2714 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
| 10 | 3, 9 | wceq 1540 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
| Colors of variables: wff setvar class |
| This definition is referenced by: dfin5 3959 elin 3967 dfss2 3969 disj 4450 iinxprg 5089 disjex 32605 disjexc 32606 eulerpartlemt 34373 in-ax8 36225 iocinico 43224 csbingVD 44904 |
| Copyright terms: Public domain | W3C validator |