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

Theorem risset 3232
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 1860 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3070 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2816 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 304 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395   = wceq 1539  wex 1778  wcel 2107  wrex 3069
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-clel 2815  df-rex 3070
This theorem is referenced by:  nelb  3233  nelbOLD  3234  ceqsralv  3521  clel5  3664  reueq  3742  reuind  3758  0el  4362  iunidOLD  5060  reusv3  5404  elidinxp  6061  sucel  6457  fvmptt  7035  releldm2  8069  qsid  8824  ttrcltr  9757  zorng  10545  rereccl  11986  nndiv  12313  incexc2  15875  ruclem12  16278  conjnmzb  19272  pgpfac1lem2  20096  pgpfac1lem4  20099  mat1dimelbas  22478  mat1dimbas  22479  chmaidscmat  22855  unisngl  23536  fmid  23969  dcubic  26890  addsrid  27998  addsprop  28010  negsprop  28068  mulsrid  28140  mulsprop  28157  fusgrn0degnn0  29518  chscllem2  31658  disjunsn  32608  grplsm0l  33432  ballotlemsima  34519  dfon2lem8  35792  brimg  35939  dfrecs2  35952  altopelaltxp  35978  prtlem9  38866  prter2  38883  2llnmat  39527  2lnat  39787  cdlemefrs29bpre1  40400  elnn0rabdioph  42819  fiphp3d  42835  minregex  43552
  Copyright terms: Public domain W3C validator