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

Theorem risset 3267
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 1852 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3144 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2894 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 305 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 207  wa 396   = wceq 1528  wex 1771  wcel 2105  wrex 3139
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-clel 2893  df-rex 3144
This theorem is referenced by:  nelb  3268  clel5  3656  reueq  3727  reuind  3743  0el  4319  iunid  4976  reusv3  5297  elidinxp  5905  sucel  6258  fvmptt  6781  releldm2  7733  qsid  8353  zorng  9915  rereccl  11347  nndiv  11672  zqOLD  12344  incexc2  15183  ruclem12  15584  conjnmzb  18333  pgpfac1lem2  19128  pgpfac1lem4  19131  mat1dimelbas  21010  mat1dimbas  21011  chmaidscmat  21386  unisngl  22065  fmid  22498  dcubic  25351  fusgrn0degnn0  27209  chscllem2  29343  disjunsn  30273  ballotlemsima  31673  dfon2lem8  32933  brimg  33296  dfrecs2  33309  altopelaltxp  33335  prtlem9  35882  prter2  35899  2llnmat  36542  2lnat  36802  cdlemefrs29bpre1  37415  elnn0rabdioph  39280  fiphp3d  39296
  Copyright terms: Public domain W3C validator