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

Theorem reurex 3414
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 3413 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 501 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3134  ∃!wreu 3135  ∃*wrmo 3136
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 210  df-an 400  df-eu 2655  df-rex 3139  df-reu 3140  df-rmo 3141
This theorem is referenced by:  2reu2rex  3415  reu3  3704  reuxfr1d  3727  2rexreu  3739  sbcreu  3843  reu0  4301  2reu4  4449  tz6.26  6166  weniso  7100  oawordex  8179  oaabs  8267  oaabs2  8268  supval2  8916  fisup2g  8929  fiinf2g  8961  nqerf  10350  qbtwnre  12589  modprm0  16140  issrgid  19273  isringid  19326  lspsneu  19895  frgpcyg  20720  qtophmeo  22425  pjthlem2  24045  dyadmax  24205  quotlem  24899  2sqreulem1  26033  2sqreunnlem1  26036  nfrgr2v  28060  2pthfrgrrn  28070  frgrncvvdeqlem9  28095  frgr2wwlkn0  28116  pjhthlem2  29178  cnlnadj  29865  2reu2rex1  30253  rmoxfrd  30266  cvmliftpht  32622  finorwe  34744  lcfl7N  38742  renegeulem  39437  resubeqsub  39495  requad1  44066  requad2  44067  isringrng  44431  uzlidlring  44479
  Copyright terms: Public domain W3C validator