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 28132). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3940) and difference (𝐴 ∖ 𝐵) (df-dif 3938). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4236 and dfin4 4243. For intersection defined in terms of union, see dfin3 4242. (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 3934 | . 2 class (𝐴 ∩ 𝐵) |
4 | vx | . . . . . 6 setvar 𝑥 | |
5 | 4 | cv 1527 | . . . . 5 class 𝑥 |
6 | 5, 1 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐴 |
7 | 5, 2 | wcel 2105 | . . . 4 wff 𝑥 ∈ 𝐵 |
8 | 6, 7 | wa 396 | . . 3 wff (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵) |
9 | 8, 4 | cab 2799 | . 2 class {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
10 | 3, 9 | wceq 1528 | 1 wff (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} |
Colors of variables: wff setvar class |
This definition is referenced by: dfin5 3943 dfss2 3954 elin 4168 disj 4397 iinxprg 5003 disjex 30271 disjexc 30272 eulerpartlemt 31529 iocinico 39698 csbingVD 41098 |
Copyright terms: Public domain | W3C validator |