![]() |
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 27412). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3612) and difference (𝐴 ∖ 𝐵) (df-dif 3610). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3893 and dfin4 3900. For intersection defined in terms of union, see dfin3 3899. (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 3606 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1522 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2030 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2030 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2637 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1523 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3615 dfss2 3624 elin 3829 disj 4050 iinxprg 4633 disjex 29531 disjexc 29532 eulerpartlemt 30561 iocinico 38114 csbingVD 39434 |
Copyright terms: Public domain | W3C validator |