Theorem reurex 3370

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3087  ∃!wreu 3364  ∃*wrmo 3365

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2595  df-rex 3088  df-rmo 3366  df-reu 3367

This theorem is used by:  2reu2rex  3378  reu3  3685  reuxfr1d  3708  2rexreu  3720  sbcreu  3823  reu0  4309  2reu4  4480  weniso  7356  oawordex  8549  oaabs  8641  oaabs2  8642  supval2  9431  fisup2g  9445  fiinf2g  9478  nqerf  10996  qbtwnre  13310  modprm0  16963  issrgid  20410  isringid  20480  isringrng  20496  lspsneu  21381  frgpcyg  21859  qtophmeo  24116  pjthlem2  25739  dyadmax  25899  quotlem  26603  2sqreulem1  27755  2sqreunnlem1  27758  angmgmaddcpbl  29372  angmgmaddcl  29373  nfrgr2v  30855  2pthfrgrrn  30865  frgrncvvdeqlem9  30890  frgr2wwlkn0  30911  pjhthlem2  31976  cnlnadj  32663  2reu2rex1  33059  rmoxfrd  33071  cvmliftpht  36052  finorwe  38273  lcfl7N  42526  renegeulem  43388  resubeqsub  43449  requad1  48664  requad2  48665  uzlidlring  49276  reuxfr1dd  49861  lubeldm2  50008  glbeldm2  50009  upciclem4  50221  ralseurals  50865