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 500	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3085  ∃!wreu 3364  ∃*wrmo 3365

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 209  df-an 400  df-eu 2595  df-rex 3086  df-rmo 3366  df-reu 3367

This theorem is referenced by:  2reu2rex  3378  reu3  3689  reuxfr1d  3712  2rexreu  3724  sbcreu  3829  reu0  4313  2reu4  4477  weniso  7334  oawordex  8521  oaabs  8613  oaabs2  8614  supval2  9398  fisup2g  9412  fiinf2g  9445  nqerf  10885  qbtwnre  13199  modprm0  16824  issrgid  20233  isringid  20300  isringrng  20316  lspsneu  21173  frgpcyg  21605  qtophmeo  23857  pjthlem2  25480  dyadmax  25640  quotlem  26341  2sqreulem1  27487  2sqreunnlem1  27490  nfrgr2v  30420  2pthfrgrrn  30430  frgrncvvdeqlem9  30455  frgr2wwlkn0  30476  pjhthlem2  31541  cnlnadj  32228  2reu2rex1  32628  rmoxfrd  32640  cvmliftpht  35632  finorwe  37840  lcfl7N  42089  renegeulem  42942  resubeqsub  43003  requad1  48208  requad2  48209  uzlidlring  48821  reuxfr1dd  49392  lubeldm2  49541  glbeldm2  49542  upciclem4  49754