Theorem reurex 3346

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

Syntax hints:   → wi 4  ∃wrex 3061  ∃!wreu 3340  ∃*wrmo 3341

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 2569  df-rex 3062  df-rmo 3342  df-reu 3343

This theorem is referenced by:  2reu2rex  3354  reu3  3673  reuxfr1d  3696  2rexreu  3708  sbcreu  3814  reu0  4301  2reu4  4464  weniso  7309  oawordex  8492  oaabs  8584  oaabs2  8585  supval2  9368  fisup2g  9382  fiinf2g  9415  nqerf  10853  qbtwnre  13151  modprm0  16776  issrgid  20185  isringid  20252  isringrng  20268  lspsneu  21121  frgpcyg  21553  qtophmeo  23782  pjthlem2  25405  dyadmax  25565  quotlem  26266  2sqreulem1  27409  2sqreunnlem1  27412  nfrgr2v  30342  2pthfrgrrn  30352  frgrncvvdeqlem9  30377  frgr2wwlkn0  30398  pjhthlem2  31463  cnlnadj  32150  2reu2rex1  32550  rmoxfrd  32562  cvmliftpht  35500  finorwe  37698  lcfl7N  41947  renegeulem  42801  resubeqsub  42862  requad1  48098  requad2  48099  uzlidlring  48711  reuxfr1dd  49282  lubeldm2  49431  glbeldm2  49432  upciclem4  49644