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

Theorem risset 3055
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 1784 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 2913 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 df-clel 2617 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 293 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  wrex 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-clel 2617  df-rex 2913
This theorem is referenced by:  reueq  3386  reuind  3393  0el  3915  iunid  4541  reusv3  4836  sucel  5757  fvmptt  6256  releldm2  7163  qsid  7758  zorng  9270  rereccl  10687  nndiv  11005  zq  11738  4fvwrd4  12400  wrdlen1  13282  incexc2  14495  ruclem12  14895  phisum  15419  conjnmzb  17616  symgmov1  17733  pgpfac1lem2  18395  pgpfac1lem4  18398  mat1dimelbas  20196  mat1dimbas  20197  chmaidscmat  20572  unisngl  21240  fmid  21674  dcubic  24473  fusgrn0degnn0  26281  chscllem2  28346  disjunsn  29252  ballotlemsima  30358  dfon2lem8  31396  brimg  31686  dfrecs2  31699  altopelaltxp  31725  prtlem9  33629  prtlem11  33631  prter2  33646  2llnmat  34290  2lnat  34550  cdlemefrs29bpre1  35165  elnn0rabdioph  36847  fiphp3d  36863
  Copyright terms: Public domain W3C validator