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

Theorem risset 2782
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 1638 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2740 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2439 . 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 1369   E.wex 1586    e. wcel 1756   E.wrex 2735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-clel 2439  df-rex 2740
This theorem is referenced by:  reueq  3175  reuind  3181  0el  3673  iunid  4244  reusv3  4519  sucel  4811  fvmptt  5808  releldm2  6643  qsid  7185  zorng  8692  rereccl  10068  nndiv  10381  zq  10978  4fvwrd4  11552  incexc2  13320  ruclem12  13542  conjnmzb  15800  symgmov1  15916  pgpfac1lem2  16595  pgpfac1lem4  16598  fmid  19552  dcubic  22260  chscllem2  25060  disjunsn  25955  ballotlemsima  26917  dfon2lem8  27622  brimg  27987  tfrqfree  28001  altopelaltxp  28026  prtlem9  29032  prtlem11  29034  prter2  29049  elnn0rabdioph  29164  fiphp3d  29181  phisum  29590  wrdlen1  30273  usgn0fidegnn0  30645  mat1dimelbas  30890  mat1dimbas  30891  2llnmat  33191  2lnat  33451  cdlemefrs29bpre1  34064
  Copyright terms: Public domain W3C validator