Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-in Structured version   Visualization version   GIF version

Definition df-in 3865
 Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, ({1, 3} ∩ {1, 8}) = {1} (ex-in 28309). Contrast this operation with union (𝐴 ∪ 𝐵) (df-un 3863) and difference (𝐴 ∖ 𝐵) (df-dif 3861). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 4165 and dfin4 4172. For intersection defined in terms of union, see dfin3 4171. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
df-in (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Detailed syntax breakdown of Definition df-in
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
31, 2cin 3857 . 2 class (𝐴𝐵)
4 vx . . . . . 6 setvar 𝑥
54cv 1537 . . . . 5 class 𝑥
65, 1wcel 2111 . . . 4 wff 𝑥𝐴
75, 2wcel 2111 . . . 4 wff 𝑥𝐵
86, 7wa 399 . . 3 wff (𝑥𝐴𝑥𝐵)
98, 4cab 2735 . 2 class {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
103, 9wceq 1538 1 wff (𝐴𝐵) = {𝑥 ∣ (𝑥𝐴𝑥𝐵)}
 Colors of variables: wff setvar class This definition is referenced by:  dfin5  3866  elin  3874  dfss2OLD  3879  ss2abdv  3968  disj  4344  disjOLD  4345  iinxprg  4976  disjex  30453  disjexc  30454  eulerpartlemt  31857  iocinico  40557  csbingVD  41985
 Copyright terms: Public domain W3C validator