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

Theorem reurex 3136
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 3135 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 474 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 2896  ∃!wreu 2897  ∃*wrmo 2898
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-eu 2461  df-mo 2462  df-rex 2901  df-reu 2902  df-rmo 2903
This theorem is referenced by:  reu3  3362  sbcreu  3481  reuxfrd  4813  tz6.26  5613  weniso  6481  oawordex  7501  oaabs  7588  oaabs2  7589  supval2  8221  fisup2g  8234  fiinf2g  8266  nqerf  9608  qbtwnre  11865  modprm0  15296  meet0  16908  join0  16909  issrgid  18294  isringid  18344  lspsneu  18892  frgpcyg  19688  qtophmeo  21377  pjthlem2  22961  dyadmax  23116  quotlem  23803  frgra2v  26319  2pthfrgrarn  26329  frgrancvvdeqlemC  26359  frg2wotn0  26376  pjhthlem2  27428  cnlnadj  28115  reuxfr4d  28507  rmoxfrdOLD  28509  rmoxfrd  28510  cvmliftpht  30347  lcfl7N  35591  2reu2rex  39615  2rexreu  39617  2reu4  39622  nfrgr2v  41423  2pthfrgrrn  41433  frgrncvvdeqlemC  41459  frgr2wwlkn0  41474  isringrng  41652  uzlidlring  41700
  Copyright terms: Public domain W3C validator