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

Theorem risset 2603
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 1576 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2562 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2292 . 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 1531    = wceq 1632    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  reueq  2975  reuind  2981  0el  3484  iunid  3973  sucel  4481  reusv3  4558  fvmptt  5631  releldm2  6186  qsid  6741  zorng  8147  rereccl  9494  nndiv  9802  zq  10338  incexc2  12313  ruclem12  12535  conjnmzb  14733  pgpfac1lem2  15326  pgpfac1lem4  15329  fmid  17671  dcubic  20158  chscllem2  22233  ballotlemsima  23090  dfon2lem8  24217  elfuns  24525  tfrqfree  24561  altopelaltxp  24582  bsstrs  26249  nbssntrs  26250  prtlem9  26835  prtlem11  26837  prter2  26852  elnn0rabdioph  26987  fiphp3d  27005  phisum  27621  4fvwrd4  28220  2llnmat  30335  2lnat  30595  cdlemefrs29bpre1  31208
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-clel 2292  df-rex 2562
  Copyright terms: Public domain W3C validator