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

Theorem risset 3044
 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 1774 . 2 (∃𝑥(𝑥𝐵𝑥 = 𝐴) ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
2 df-rex 2902 . 2 (∃𝑥𝐵 𝑥 = 𝐴 ↔ ∃𝑥(𝑥𝐵𝑥 = 𝐴))
3 df-clel 2606 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
41, 2, 33bitr4ri 292 1 (𝐴𝐵 ↔ ∃𝑥𝐵 𝑥 = 𝐴)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  ∃wrex 2897 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728 This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-clel 2606  df-rex 2902 This theorem is referenced by:  reueq  3371  reuind  3378  0el  3895  iunid  4511  reusv3  4802  sucel  5715  fvmptt  6208  releldm2  7109  qsid  7700  zorng  9209  rereccl  10622  nndiv  10938  zq  11670  4fvwrd4  12328  wrdlen1  13198  incexc2  14409  ruclem12  14809  phisum  15333  conjnmzb  17518  symgmov1  17635  pgpfac1lem2  18297  pgpfac1lem4  18300  mat1dimelbas  20096  mat1dimbas  20097  chmaidscmat  20472  unisngl  21140  fmid  21574  dcubic  24373  usgn0fidegnn0  26556  chscllem2  27881  disjunsn  28789  ballotlemsima  29904  dfon2lem8  30939  brimg  31214  dfrecs2  31227  altopelaltxp  31253  prtlem9  33167  prtlem11  33169  prter2  33184  2llnmat  33828  2lnat  34088  cdlemefrs29bpre1  34703  elnn0rabdioph  36385  fiphp3d  36401  fusgrn0degnn0  40714
 Copyright terms: Public domain W3C validator