![]() |
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 30234). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3952) and difference (𝐴 ∖ 𝐵) (df-dif 3950). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4261 and dfin4 4268. For intersection defined in terms of union, see dfin3 4267. (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 3946 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1533 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2099 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 395 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2705 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1534 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3955 elin 3963 ss2abdv 4058 disj 4448 disjOLD 4449 iinxprg 5092 disjex 32381 disjexc 32382 eulerpartlemt 33991 iocinico 42640 csbingVD 44323 |
Copyright terms: Public domain | W3C validator |