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

Theorem risset 3207
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 1862 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3057 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2807 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 304 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1541  wex 1780  wcel 2111  wrex 3056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-clel 2806  df-rex 3057
This theorem is referenced by:  nelb  3208  ceqsralv  3477  clel5  3615  reueq  3691  reuind  3707  0el  4310  reusv3  5341  elidinxp  5992  sucel  6382  fvmptt  6949  releldm2  7975  qsid  8705  ttrcltr  9606  zorng  10395  rereccl  11839  nndiv  12171  incexc2  15745  ruclem12  16150  chnfi  18540  conjnmzb  19165  pgpfac1lem2  19989  pgpfac1lem4  19992  mat1dimelbas  22386  mat1dimbas  22387  chmaidscmat  22763  unisngl  23442  fmid  23875  dcubic  26783  addsrid  27907  addsprop  27919  negsprop  27977  mulsrid  28052  mulsprop  28069  onsfi  28283  fusgrn0degnn0  29478  chscllem2  31618  disjunsn  32574  grplsm0l  33368  ballotlemsima  34529  dfon2lem8  35832  brimg  35979  dfrecs2  35994  altopelaltxp  36020  prtlem9  38962  prter2  38979  2llnmat  39622  2lnat  39882  cdlemefrs29bpre1  40495  elnn0rabdioph  42895  fiphp3d  42911  minregex  43626
  Copyright terms: Public domain W3C validator