MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfin5 Structured version   Unicode version

Theorem dfin5 3450
Description: Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.)
Assertion
Ref Expression
dfin5  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
Distinct variable groups:    x, A    x, B

Proof of Theorem dfin5
StepHypRef Expression
1 df-in 3449 . 2  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
2 df-rab 2791 . 2  |-  { x  e.  A  |  x  e.  B }  =  {
x  |  ( x  e.  A  /\  x  e.  B ) }
31, 2eqtr4i 2461 1  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
Colors of variables: wff setvar class
Syntax hints:    /\ wa 370    = wceq 1437    e. wcel 1870   {cab 2414   {crab 2786    i^i cin 3441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-cleq 2421  df-rab 2791  df-in 3449
This theorem is referenced by:  nfin  3675  rabbi2dva  3676  dfepfr  4839  epfrc  4840  pmtrmvd  17048  ablfaclem3  17655  mretopd  20039  ptclsg  20561  xkopt  20601  iscmet3  22156  xrlimcnp  23759  ppiub  23995  suppss2fOLD  28077  xppreima  28088  fpwrelmapffs  28162  orvcelval  29127  sstotbnd2  31813  glbconN  32654  2polssN  33192
  Copyright terms: Public domain W3C validator