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

Theorem risset 2590
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 1573 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2549 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2279 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
41, 2, 33bitr4ri 269 1  |-  ( A  e.  B  <->  E. x  e.  B  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  reueq  2962  reuind  2968  0el  3471  iunid  3957  sucel  4465  reusv3  4542  fvmptt  5615  releldm2  6170  qsid  6725  zorng  8131  rereccl  9478  nndiv  9786  zq  10322  incexc2  12297  ruclem12  12519  conjnmzb  14717  pgpfac1lem2  15310  pgpfac1lem4  15313  fmid  17655  dcubic  20142  chscllem2  22217  ballotlemsima  23074  dfon2lem8  24146  elfuns  24454  tfrqfree  24489  altopelaltxp  24510  bsstrs  26146  nbssntrs  26147  prtlem9  26732  prtlem11  26734  prter2  26749  elnn0rabdioph  26884  fiphp3d  26902  phisum  27518  2llnmat  29713  2lnat  29973  cdlemefrs29bpre1  30586
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-clel 2279  df-rex 2549
  Copyright terms: Public domain W3C validator