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

Theorem risset 3247
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 1905 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3096 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 df-clel 2774 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 296 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386   = wceq 1601  wex 1823  wcel 2107  wrex 3091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853
This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824  df-clel 2774  df-rex 3096
This theorem is referenced by:  clel5  3547  reueq  3618  reuind  3628  0el  4169  iunid  4810  reusv3  5119  elidinxp  5707  sucel  6051  fvmptt  6563  releldm2  7499  qsid  8098  zorng  9663  rereccl  11096  nndiv  11426  zqOLD  12107  incexc2  14983  ruclem12  15383  conjnmzb  18090  pgpfac1lem2  18872  pgpfac1lem4  18875  mat1dimelbas  20693  mat1dimbas  20694  chmaidscmat  21071  unisngl  21750  fmid  22183  dcubic  25035  fusgrn0degnn0  26864  chscllem2  29086  disjunsn  29987  ballotlemsima  31184  dfon2lem8  32291  brimg  32641  dfrecs2  32654  altopelaltxp  32680  prtlem9  35027  prtlem11  35029  prter2  35044  2llnmat  35687  2lnat  35947  cdlemefrs29bpre1  36560  elnn0rabdioph  38341  fiphp3d  38357
  Copyright terms: Public domain W3C validator