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

Theorem reurex 3190
 Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)
Assertion
Ref Expression
reurex (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)

Proof of Theorem reurex
StepHypRef Expression
1 reu5 3189 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 475 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∃wrex 2942  ∃!wreu 2943  ∃*wrmo 2944 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-eu 2502  df-mo 2503  df-rex 2947  df-reu 2948  df-rmo 2949 This theorem is referenced by:  reu3  3429  sbcreu  3548  reuxfrd  4923  tz6.26  5749  weniso  6644  oawordex  7682  oaabs  7769  oaabs2  7770  supval2  8402  fisup2g  8415  fiinf2g  8447  nqerf  9790  qbtwnre  12068  modprm0  15557  meet0  17184  join0  17185  issrgid  18569  isringid  18619  lspsneu  19171  frgpcyg  19970  qtophmeo  21668  pjthlem2  23255  dyadmax  23412  quotlem  24100  nfrgr2v  27252  2pthfrgrrn  27262  frgrncvvdeqlem9  27287  frgr2wwlkn0  27308  pjhthlem2  28379  cnlnadj  29066  reuxfr4d  29457  rmoxfrdOLD  29459  rmoxfrd  29460  cvmliftpht  31426  lcfl7N  37107  2reu2rex  41504  2rexreu  41506  2reu4  41511  isringrng  42206  uzlidlring  42254
 Copyright terms: Public domain W3C validator