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

Theorem risset 3231
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 1859 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3069 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2815 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 304 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1537  wex 1776  wcel 2106  wrex 3068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-clel 2814  df-rex 3069
This theorem is referenced by:  nelb  3232  nelbOLD  3233  ceqsralv  3520  clel5  3665  reueq  3746  reuind  3762  0el  4369  iunidOLD  5066  reusv3  5411  elidinxp  6064  sucel  6460  fvmptt  7036  releldm2  8067  qsid  8822  ttrcltr  9754  zorng  10542  rereccl  11983  nndiv  12310  incexc2  15871  ruclem12  16274  conjnmzb  19284  pgpfac1lem2  20110  pgpfac1lem4  20113  mat1dimelbas  22493  mat1dimbas  22494  chmaidscmat  22870  unisngl  23551  fmid  23984  dcubic  26904  addsrid  28012  addsprop  28024  negsprop  28082  mulsrid  28154  mulsprop  28171  fusgrn0degnn0  29532  chscllem2  31667  disjunsn  32614  grplsm0l  33411  ballotlemsima  34497  dfon2lem8  35772  brimg  35919  dfrecs2  35932  altopelaltxp  35958  prtlem9  38846  prter2  38863  2llnmat  39507  2lnat  39767  cdlemefrs29bpre1  40380  elnn0rabdioph  42791  fiphp3d  42807  minregex  43524
  Copyright terms: Public domain W3C validator