![]() |
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 27585). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3712) and difference (𝐴 ∖ 𝐵) (df-dif 3710). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3995 and dfin4 4002. For intersection defined in terms of union, see dfin3 4001. (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 3706 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1623 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2131 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2131 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 383 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2738 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1624 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3715 dfss2 3724 elin 3931 disj 4152 iinxprg 4745 disjex 29704 disjexc 29705 eulerpartlemt 30734 iocinico 38291 csbingVD 39611 |
Copyright terms: Public domain | W3C validator |