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

Theorem dfin5 3330
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 3329 . 2  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
2 df-rab 2716 . 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 set class
Syntax hints:    /\ wa 360    = wceq 1653    e. wcel 1726   {cab 2424   {crab 2711    i^i cin 3321
This theorem is referenced by:  nfin  3549  rabbi2dva  3551  dfepfr  4569  epfrc  4570  ablfaclem3  15647  mretopd  17158  ptclsg  17649  xkopt  17689  iscmet3  19248  xrlimcnp  20809  ppiub  20990  suppss2f  24051  xppreima  24061  orvcelval  24728  sstotbnd2  26485  pmtrmvd  27377  glbconN  30236  2polssN  30774
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-cleq 2431  df-rab 2716  df-in 3329
  Copyright terms: Public domain W3C validator