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

Theorem reurex 3368
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 3366 . 2 (∃!𝑥𝐴 𝜑 ↔ (∃𝑥𝐴 𝜑 ∧ ∃*𝑥𝐴 𝜑))
21simplbi 496 1 (∃!𝑥𝐴 𝜑 → ∃𝑥𝐴 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wrex 3060  ∃!wreu 3362  ∃*wrmo 3363
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 395  df-eu 2558  df-rex 3061  df-rmo 3364  df-reu 3365
This theorem is referenced by:  2reu2rex  3378  reu3  3720  reuxfr1d  3743  2rexreu  3755  sbcreu  3868  reu0  4354  2reu4  4521  tz6.26OLD  6353  weniso  7358  oawordex  8579  oaabs  8670  oaabs2  8671  supval2  9491  fisup2g  9504  fiinf2g  9536  nqerf  10964  qbtwnre  13226  modprm0  16802  issrgid  20183  isringid  20246  isringrng  20262  lspsneu  21100  frgpcyg  21567  qtophmeo  23809  pjthlem2  25454  dyadmax  25615  quotlem  26325  2sqreulem1  27472  2sqreunnlem1  27475  nfrgr2v  30202  2pthfrgrrn  30212  frgrncvvdeqlem9  30237  frgr2wwlkn0  30258  pjhthlem2  31322  cnlnadj  32009  2reu2rex1  32406  rmoxfrd  32418  cvmliftpht  35159  finorwe  37102  lcfl7N  41213  renegeulem  42080  resubeqsub  42140  requad1  47230  requad2  47231  uzlidlring  47648  lubeldm2  48326  glbeldm2  48327
  Copyright terms: Public domain W3C validator