Theorem reurex 3356

Description: Restricted unique existence implies restricted existence. (Contributed by NM, 19-Aug-1999.)

Assertion

Ref	Expression
reurex	⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Proof of Theorem reurex

Step	Hyp	Ref	Expression
1		reu5 3354	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2	1	simplbi 496	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3062  ∃!wreu 3350  ∃*wrmo 3351

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 207  df-an 396  df-eu 2570  df-rex 3063  df-rmo 3352  df-reu 3353

This theorem is referenced by:  2reu2rex  3364  reu3  3687  reuxfr1d  3710  2rexreu  3722  sbcreu  3828  reu0  4315  2reu4  4479  weniso  7310  oawordex  8494  oaabs  8586  oaabs2  8587  supval2  9370  fisup2g  9384  fiinf2g  9417  nqerf  10853  qbtwnre  13126  modprm0  16745  issrgid  20151  isringid  20218  isringrng  20234  lspsneu  21090  frgpcyg  21540  qtophmeo  23773  pjthlem2  25406  dyadmax  25567  quotlem  26276  2sqreulem1  27425  2sqreunnlem1  27428  nfrgr2v  30359  2pthfrgrrn  30369  frgrncvvdeqlem9  30394  frgr2wwlkn0  30415  pjhthlem2  31479  cnlnadj  32166  2reu2rex1  32566  rmoxfrd  32578  cvmliftpht  35531  finorwe  37631  lcfl7N  41871  renegeulem  42733  resubeqsub  42794  requad1  47976  requad2  47977  uzlidlring  48589  reuxfr1dd  49160  lubeldm2  49309  glbeldm2  49310  upciclem4  49522