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

Theorem reurex 3371
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 3370 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 490 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3089  ∃!wreu 3090  ∃*wrmo 3091
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 199  df-an 388  df-eu 2583  df-rex 3094  df-reu 3095  df-rmo 3096
This theorem is referenced by:  2reu2rex  3372  reu3  3632  reuxfr4d  3654  2rexreu  3664  sbcreu  3764  reu0  4206  2reu4  4350  reuxfrd  5175  tz6.26  6019  weniso  6932  oawordex  7986  oaabs  8073  oaabs2  8074  supval2  8716  fisup2g  8729  fiinf2g  8761  nqerf  10152  qbtwnre  12412  modprm0  16001  issrgid  18999  isringid  19049  lspsneu  19620  frgpcyg  20425  qtophmeo  22132  pjthlem2  23747  dyadmax  23905  quotlem  24595  2sqreulem1  25727  2sqreunnlem1  25730  nfrgr2v  27809  2pthfrgrrn  27819  frgrncvvdeqlem9  27844  frgr2wwlkn0  27865  pjhthlem2  28953  cnlnadj  29640  2reu2rex1  30029  rmoxfrd  30041  cvmliftpht  32150  lcfl7N  38082  renegeulem  38631  requad1  43156  requad2  43157  isringrng  43517  uzlidlring  43565
  Copyright terms: Public domain W3C validator