Theorem reurex 3351

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

Syntax hints:   → wi 4  ∃wrex 3057  ∃!wreu 3345  ∃*wrmo 3346

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 2566  df-rex 3058  df-rmo 3347  df-reu 3348

This theorem is referenced by:  2reu2rex  3359  reu3  3682  reuxfr1d  3705  2rexreu  3717  sbcreu  3823  reu0  4310  2reu4  4472  weniso  7294  oawordex  8478  oaabs  8569  oaabs2  8570  supval2  9346  fisup2g  9360  fiinf2g  9393  nqerf  10828  qbtwnre  13100  modprm0  16719  issrgid  20124  isringid  20191  isringrng  20207  lspsneu  21062  frgpcyg  21512  qtophmeo  23733  pjthlem2  25366  dyadmax  25527  quotlem  26236  2sqreulem1  27385  2sqreunnlem1  27388  nfrgr2v  30254  2pthfrgrrn  30264  frgrncvvdeqlem9  30289  frgr2wwlkn0  30310  pjhthlem2  31374  cnlnadj  32061  2reu2rex1  32462  rmoxfrd  32474  cvmliftpht  35383  finorwe  37447  lcfl7N  41620  renegeulem  42487  resubeqsub  42548  requad1  47746  requad2  47747  uzlidlring  48359  reuxfr1dd  48931  lubeldm2  49080  glbeldm2  49081  upciclem4  49294