Theorem reurex 3374

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 3372	. 2 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 ↔ (∃𝑥 ∈ 𝐴 𝜑 ∧ ∃*𝑥 ∈ 𝐴 𝜑))
2	1	simplbi 501	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3089  ∃!wreu 3368  ∃*wrmo 3369

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 401  df-eu 2599  df-rex 3090  df-rmo 3370  df-reu 3371

This theorem is referenced by:  2reu2rex  3382  reu3  3693  reuxfr1d  3716  2rexreu  3728  sbcreu  3832  reu0  4317  2reu4  4481  weniso  7342  oawordex  8530  oaabs  8622  oaabs2  8623  supval2  9403  fisup2g  9417  fiinf2g  9450  nqerf  10903  qbtwnre  13216  modprm0  16855  issrgid  20277  isringid  20345  isringrng  20361  lspsneu  21216  frgpcyg  21683  qtophmeo  23935  pjthlem2  25558  dyadmax  25718  quotlem  26422  2sqreulem1  27568  2sqreunnlem1  27571  nfrgr2v  30532  2pthfrgrrn  30542  frgrncvvdeqlem9  30567  frgr2wwlkn0  30588  pjhthlem2  31653  cnlnadj  32340  2reu2rex1  32737  rmoxfrd  32749  cvmliftpht  35681  finorwe  37888  lcfl7N  42137  renegeulem  42990  resubeqsub  43051  requad1  48242  requad2  48243  uzlidlring  48855  reuxfr1dd  49436  lubeldm2  49585  glbeldm2  49586  upciclem4  49798