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

Theorem risset 3260
 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 1862 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 3139 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 dfclel 2897 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 307 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538  ∃wex 1781   ∈ wcel 2115  ∃wrex 3134 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-clel 2896  df-rex 3139 This theorem is referenced by:  nelb  3261  clel5  3643  reueq  3714  reuind  3730  0el  4302  iunid  4970  reusv3  5293  elidinxp  5898  sucel  6251  fvmptt  6776  releldm2  7732  qsid  8353  zorng  9918  rereccl  11350  nndiv  11676  incexc2  15189  ruclem12  15590  conjnmzb  18389  pgpfac1lem2  19193  pgpfac1lem4  19196  mat1dimelbas  21073  mat1dimbas  21074  chmaidscmat  21449  unisngl  22128  fmid  22561  dcubic  25428  fusgrn0degnn0  27285  chscllem2  29417  disjunsn  30348  ballotlemsima  31798  dfon2lem8  33060  brimg  33423  dfrecs2  33436  altopelaltxp  33462  prtlem9  36070  prter2  36087  2llnmat  36730  2lnat  36990  cdlemefrs29bpre1  37603  elnn0rabdioph  39597  fiphp3d  39613
 Copyright terms: Public domain W3C validator