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

Theorem dfin5 3173
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 3172 . 2  |-  ( A  i^i  B )  =  { x  |  ( x  e.  A  /\  x  e.  B ) }
2 df-rab 2565 . 2  |-  { x  e.  A  |  x  e.  B }  =  {
x  |  ( x  e.  A  /\  x  e.  B ) }
31, 2eqtr4i 2319 1  |-  ( A  i^i  B )  =  { x  e.  A  |  x  e.  B }
Colors of variables: wff set class
Syntax hints:    /\ wa 358    = wceq 1632    e. wcel 1696   {cab 2282   {crab 2560    i^i cin 3164
This theorem is referenced by:  nfin  3388  rabbi2dva  3390  dfepfr  4394  epfrc  4395  ablfaclem3  15338  mretopd  16845  ptclsg  17325  xkopt  17365  iscmet3  18735  xrlimcnp  20279  ppiub  20459  suppss2f  23216  xppreima  23226  orvcelval  23684  sstotbnd2  26601  pmtrmvd  27501  glbconN  30188  2polssN  30726
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-rab 2565  df-in 3172
  Copyright terms: Public domain W3C validator