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

Theorem risset 3200
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 1936 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3056 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 df-clel 2756 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 293 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  wex 1853  wcel 2139  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-clel 2756  df-rex 3056
This theorem is referenced by:  reueq  3545  reuind  3552  0el  4082  iunid  4727  reusv3  5025  sucel  5959  fvmptt  6462  releldm2  7385  qsid  7980  zorng  9518  rereccl  10935  nndiv  11253  zq  11987  4fvwrd4  12653  wrdlen1  13530  incexc2  14769  ruclem12  15169  phisum  15697  conjnmzb  17896  symgmov1  18012  pgpfac1lem2  18674  pgpfac1lem4  18677  mat1dimelbas  20479  mat1dimbas  20480  chmaidscmat  20855  unisngl  21532  fmid  21965  dcubic  24772  fusgrn0degnn0  26605  chscllem2  28806  disjunsn  29714  ballotlemsima  30886  dfon2lem8  32000  brimg  32350  dfrecs2  32363  altopelaltxp  32389  prtlem9  34653  prtlem11  34655  prter2  34670  2llnmat  35313  2lnat  35573  cdlemefrs29bpre1  36187  elnn0rabdioph  37869  fiphp3d  37885
  Copyright terms: Public domain W3C validator