![]() |
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 30222). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3949) and difference (𝐴 ∖ 𝐵) (df-dif 3947). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4256 and dfin4 4263. For intersection defined in terms of union, see dfin3 4262. (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 3943 | . 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 2704 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1534 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3952 elin 3960 dfss2OLD 3965 ss2abdv 4056 disj 4443 disjOLD 4444 iinxprg 5086 disjex 32367 disjexc 32368 eulerpartlemt 33927 iocinico 42563 csbingVD 44246 |
Copyright terms: Public domain | W3C validator |