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

Theorem risset 2987
Description: Two ways to say " A belongs to  B." (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
risset  |-  ( A  e.  B  <->  E. x  e.  B  x  =  A )
Distinct variable groups:    x, A    x, B

Proof of Theorem risset
StepHypRef Expression
1 exancom 1648 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2820 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2462 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
41, 2, 33bitr4ri 278 1  |-  ( A  e.  B  <->  E. x  e.  B  x  =  A )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    = wceq 1379   E.wex 1596    e. wcel 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-clel 2462  df-rex 2820
This theorem is referenced by:  reueq  3301  reuind  3307  0el  3802  iunid  4380  reusv3  4655  sucel  4951  fvmptt  5963  releldm2  6831  qsid  7374  zorng  8880  rereccl  10258  nndiv  10572  zq  11184  4fvwrd4  11786  wrdlen1  12540  incexc2  13609  ruclem12  13831  conjnmzb  16096  symgmov1  16212  pgpfac1lem2  16916  pgpfac1lem4  16919  mat1dimelbas  18740  mat1dimbas  18741  chmaidscmat  19116  fmid  20196  dcubic  22905  usgn0fidegnn0  24706  chscllem2  26232  disjunsn  27126  ballotlemsima  28094  dfon2lem8  28799  brimg  29164  tfrqfree  29178  altopelaltxp  29203  prtlem9  30209  prtlem11  30211  prter2  30226  elnn0rabdioph  30340  fiphp3d  30357  phisum  30764  2llnmat  34320  2lnat  34580  cdlemefrs29bpre1  35193
  Copyright terms: Public domain W3C validator