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

Theorem risset 2745
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 1596 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2703 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2431 . 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 1550    = wceq 1652    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  reueq  3123  reuind  3129  0el  3636  iunid  4138  sucel  4646  reusv3  4723  fvmptt  5812  releldm2  6389  qsid  6962  zorng  8376  rereccl  9724  nndiv  10032  zq  10572  4fvwrd4  11113  incexc2  12610  ruclem12  12832  conjnmzb  15032  pgpfac1lem2  15625  pgpfac1lem4  15628  fmid  17984  dcubic  20678  chscllem2  23132  ballotlemsima  24765  dfon2lem8  25409  brimg  25774  tfrqfree  25788  altopelaltxp  25813  prtlem9  26704  prtlem11  26706  prter2  26721  elnn0rabdioph  26854  fiphp3d  26871  phisum  27486  2llnmat  30258  2lnat  30518  cdlemefrs29bpre1  31131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-clel 2431  df-rex 2703
  Copyright terms: Public domain W3C validator