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