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

Theorem reurex 3360
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 3358 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 499 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3074  ∃!wreu 3354  ∃*wrmo 3355
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 206  df-an 398  df-eu 2568  df-rex 3075  df-rmo 3356  df-reu 3357
This theorem is referenced by:  2reu2rex  3370  reu3  3690  reuxfr1d  3713  2rexreu  3725  sbcreu  3837  reu0  4323  2reu4  4489  tz6.26OLD  6307  weniso  7304  oawordex  8509  oaabs  8599  oaabs2  8600  supval2  9398  fisup2g  9411  fiinf2g  9443  nqerf  10873  qbtwnre  13125  modprm0  16684  issrgid  19942  isringid  20001  lspsneu  20600  frgpcyg  20996  qtophmeo  23184  pjthlem2  24818  dyadmax  24978  quotlem  25676  2sqreulem1  26810  2sqreunnlem1  26813  nfrgr2v  29258  2pthfrgrrn  29268  frgrncvvdeqlem9  29293  frgr2wwlkn0  29314  pjhthlem2  30376  cnlnadj  31063  2reu2rex1  31451  rmoxfrd  31463  cvmliftpht  33952  finorwe  35882  lcfl7N  39993  renegeulem  40867  resubeqsub  40927  requad1  45888  requad2  45889  isringrng  46253  uzlidlring  46301  lubeldm2  47063  glbeldm2  47064
  Copyright terms: Public domain W3C validator