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

Theorem risset 3229
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 1863 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3070 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2810 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 304 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 205  wa 395   = wceq 1540  wex 1780  wcel 2105  wrex 3069
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 1912  ax-6 1970  ax-7 2010  ax-8 2107
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-clel 2809  df-rex 3070
This theorem is referenced by:  nelb  3230  nelbOLD  3231  ceqsralv  3513  clel5  3655  reueq  3733  reuind  3749  0el  4360  iunidOLD  5064  reusv3  5403  elidinxp  6043  sucel  6438  fvmptt  7018  releldm2  8033  qsid  8783  ttrcltr  9717  zorng  10505  rereccl  11939  nndiv  12265  incexc2  15791  ruclem12  16191  conjnmzb  19174  pgpfac1lem2  19993  pgpfac1lem4  19996  mat1dimelbas  22293  mat1dimbas  22294  chmaidscmat  22670  unisngl  23351  fmid  23784  dcubic  26692  addsrid  27794  addsprop  27806  negsprop  27860  mulsrid  27926  mulsprop  27943  fusgrn0degnn0  29189  chscllem2  31324  disjunsn  32258  grplsm0l  32953  ballotlemsima  33978  dfon2lem8  35232  brimg  35379  dfrecs2  35392  altopelaltxp  35418  prtlem9  38198  prter2  38215  2llnmat  38859  2lnat  39119  cdlemefrs29bpre1  39732  elnn0rabdioph  42004  fiphp3d  42020  minregex  42748
  Copyright terms: Public domain W3C validator