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

Theorem risset 3220
Description: Two ways to say "𝐴 belongs to 𝐵". (Contributed by NM, 22-Nov-1994.)
Assertion
Ref Expression
risset (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Proof of Theorem risset
StepHypRef Expression
1 exancom 1865 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3071 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2812 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 304 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 397   = wceq 1542  wex 1782  wcel 2107  wrex 3070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-clel 2811  df-rex 3071
This theorem is referenced by:  nelb  3221  nelbOLD  3222  ceqsralv  3482  clel5  3618  reueq  3696  reuind  3712  0el  4321  iunidOLD  5022  reusv3  5361  elidinxp  5998  sucel  6392  fvmptt  6969  releldm2  7976  qsid  8725  ttrcltr  9657  zorng  10445  rereccl  11878  nndiv  12204  incexc2  15728  ruclem12  16128  conjnmzb  19048  pgpfac1lem2  19859  pgpfac1lem4  19862  mat1dimelbas  21836  mat1dimbas  21837  chmaidscmat  22213  unisngl  22894  fmid  23327  dcubic  26212  addsrid  27298  addsprop  27310  negsprop  27355  mulsrid  27399  mulslid  27400  fusgrn0degnn0  28489  chscllem2  30622  disjunsn  31558  grplsm0l  32232  ballotlemsima  33172  dfon2lem8  34421  brimg  34568  dfrecs2  34581  altopelaltxp  34607  prtlem9  37372  prter2  37389  2llnmat  38033  2lnat  38293  cdlemefrs29bpre1  38906  elnn0rabdioph  41169  fiphp3d  41185  minregex  41894
  Copyright terms: Public domain W3C validator