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

Theorem risset 2931
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 1692 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2759 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2397 . 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 367    = wceq 1405   E.wex 1633    e. wcel 1842   E.wrex 2754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1634  df-clel 2397  df-rex 2759
This theorem is referenced by:  reueq  3246  reuind  3252  0el  3755  iunid  4325  reusv3  4601  sucel  5482  fvmptt  5948  releldm2  6833  qsid  7413  zorng  8915  rereccl  10302  nndiv  10616  zq  11232  4fvwrd4  11846  wrdlen1  12630  incexc2  13799  ruclem12  14181  conjnmzb  16623  symgmov1  16739  pgpfac1lem2  17444  pgpfac1lem4  17447  mat1dimelbas  19263  mat1dimbas  19264  chmaidscmat  19639  unisngl  20318  fmid  20751  dcubic  23500  usgn0fidegnn0  25433  chscllem2  26956  disjunsn  27872  ballotlemsima  28946  dfon2lem8  29996  brimg  30262  dfrecs2  30275  altopelaltxp  30301  prtlem9  31867  prtlem11  31869  prter2  31884  2llnmat  32521  2lnat  32781  cdlemefrs29bpre1  33396  elnn0rabdioph  35078  fiphp3d  35094  phisum  35503
  Copyright terms: Public domain W3C validator