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

Theorem dfin5 3351
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 3350 . 2  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
2 df-rab 2739 . 2  |-  { x  e.  A  |  x  e.  B }  =  {
x  |  ( x  e.  A  /\  x  e.  B ) }
31, 2eqtr4i 2466 1  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369    e. wcel 1756   {cab 2429   {crab 2734    i^i cin 3342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436  df-rab 2739  df-in 3350
This theorem is referenced by:  nfin  3572  rabbi2dva  3573  dfepfr  4720  epfrc  4721  pmtrmvd  15977  ablfaclem3  16603  mretopd  18711  ptclsg  19203  xkopt  19243  iscmet3  20819  xrlimcnp  22377  ppiub  22558  suppss2f  25969  xppreima  25979  fpwrelmapffs  26049  orvcelval  26866  sstotbnd2  28692  glbconN  33040  2polssN  33578
  Copyright terms: Public domain W3C validator