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

Theorem risset 2696
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 1593 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2655 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2383 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
41, 2, 33bitr4ri 270 1  |-  ( A  e.  B  <->  E. x  e.  B  x  =  A )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359   E.wex 1547    = wceq 1649    e. wcel 1717   E.wrex 2650
This theorem is referenced by:  reueq  3074  reuind  3080  0el  3587  iunid  4087  sucel  4595  reusv3  4671  fvmptt  5759  releldm2  6336  qsid  6906  zorng  8317  rereccl  9664  nndiv  9972  zq  10512  4fvwrd4  11051  incexc2  12545  ruclem12  12767  conjnmzb  14967  pgpfac1lem2  15560  pgpfac1lem4  15563  fmid  17913  dcubic  20553  chscllem2  22988  ballotlemsima  24552  dfon2lem8  25170  elfuns  25478  tfrqfree  25514  altopelaltxp  25535  prtlem9  26404  prtlem11  26406  prter2  26421  elnn0rabdioph  26554  fiphp3d  26571  phisum  27187  2llnmat  29638  2lnat  29898  cdlemefrs29bpre1  30511
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-clel 2383  df-rex 2655
  Copyright terms: Public domain W3C validator