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 26674). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3545) and difference (𝐴 ∖ 𝐵) (df-dif 3543). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3822 and dfin4 3826. For intersection defined in terms of union, see dfin3 3825. (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 3539 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1474 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 1977 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2596 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1475 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3548 dfss2 3557 elin 3758 disj 3969 iinxprg 4537 disjex 28787 disjexc 28788 eulerpartlemt 29760 iocinico 36816 csbingVD 38142 |
Copyright terms: Public domain | W3C validator |