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

Definition df-in 3482
Description: Define the intersection of two classes. Definition 5.6 of [TakeutiZaring] p. 16. For example, (ex-in 25146). Contrast this operation with union (df-un 3480) and difference (df-dif 3478). For alternate definitions in terms of class difference, requiring no dummy variables, see dfin2 3733 and dfin4 3737. For intersection defined in terms of union, see dfin3 3736. (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
2 cB . . 3
31, 2cin 3474 . 2
4 vx . . . . . 6
54cv 1394 . . . . 5
65, 1wcel 1818 . . . 4
75, 2wcel 1818 . . . 4
86, 7wa 369 . . 3
98, 4cab 2442 . 2
103, 9wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  dfin5  3483  dfss2  3492  elin  3686  disj  3867  iinxprg  4408  disjex  27451  disjexc  27452  eulerpartlemt  28310  iocinico  31179  csbingVD  33684
  Copyright terms: Public domain W3C validator