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

Theorem risset 2968
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 1658 . 2  |-  ( E. x ( x  e.  B  /\  x  =  A )  <->  E. x
( x  =  A  /\  x  e.  B
) )
2 df-rex 2799 . 2  |-  ( E. x  e.  B  x  =  A  <->  E. x
( x  e.  B  /\  x  =  A
) )
3 df-clel 2438 . 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 1383   E.wex 1599    e. wcel 1804   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-clel 2438  df-rex 2799
This theorem is referenced by:  reueq  3283  reuind  3289  0el  3788  iunid  4370  reusv3  4645  sucel  4941  fvmptt  5956  releldm2  6835  qsid  7379  zorng  8887  rereccl  10269  nndiv  10583  zq  11199  4fvwrd4  11804  wrdlen1  12561  incexc2  13632  ruclem12  13956  conjnmzb  16280  symgmov1  16396  pgpfac1lem2  17105  pgpfac1lem4  17108  mat1dimelbas  18951  mat1dimbas  18952  chmaidscmat  19327  unisngl  20006  fmid  20439  dcubic  23155  usgn0fidegnn0  25007  chscllem2  26534  disjunsn  27431  ballotlemsima  28432  dfon2lem8  29198  brimg  29563  tfrqfree  29577  altopelaltxp  29602  prtlem9  30581  prtlem11  30583  prter2  30598  elnn0rabdioph  30712  fiphp3d  30729  phisum  31135  2llnmat  35123  2lnat  35383  cdlemefrs29bpre1  35998
  Copyright terms: Public domain W3C validator