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

Theorem dfin5 3484
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 3483 . 2  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
2 df-rab 2823 . 2  |-  { x  e.  A  |  x  e.  B }  =  {
x  |  ( x  e.  A  /\  x  e.  B ) }
31, 2eqtr4i 2499 1  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1379    e. wcel 1767   {cab 2452   {crab 2818    i^i cin 3475
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-rab 2823  df-in 3483
This theorem is referenced by:  nfin  3705  rabbi2dva  3706  dfepfr  4864  epfrc  4865  pmtrmvd  16287  ablfaclem3  16940  mretopd  19387  ptclsg  19879  xkopt  19919  iscmet3  21495  xrlimcnp  23054  ppiub  23235  suppss2f  27178  xppreima  27187  fpwrelmapffs  27257  orvcelval  28075  sstotbnd2  29901  iccintsng  31155  glbconN  34191  2polssN  34729
  Copyright terms: Public domain W3C validator