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

Theorem risset 3250
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 1947 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3102 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 df-clel 2802 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 295 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2156  wrex 3097
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-clel 2802  df-rex 3102
This theorem is referenced by:  reueq  3602  reuind  3609  0el  4140  iunid  4767  reusv3  5074  elidinxp  5660  sucel  6010  fvmptt  6517  releldm2  7446  qsid  8044  zorng  9607  rereccl  11024  nndiv  11343  zq  12009  4fvwrd4  12679  wrdlen1  13551  incexc2  14788  ruclem12  15186  phisum  15708  conjnmzb  17893  symgmov1  18009  pgpfac1lem2  18672  pgpfac1lem4  18675  mat1dimelbas  20485  mat1dimbas  20486  chmaidscmat  20863  unisngl  21541  fmid  21974  dcubic  24786  fusgrn0degnn0  26622  chscllem2  28824  disjunsn  29731  ballotlemsima  30901  dfon2lem8  32013  brimg  32363  dfrecs2  32376  altopelaltxp  32402  prtlem9  34641  prtlem11  34643  prter2  34658  2llnmat  35302  2lnat  35562  cdlemefrs29bpre1  36175  elnn0rabdioph  37866  fiphp3d  37882
  Copyright terms: Public domain W3C validator