Theorem reurex 3348

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

Syntax hints:   → wi 4  ∃wrex 3063  ∃!wreu 3342  ∃*wrmo 3343

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 208  df-an 397  df-eu 2573  df-rex 3064  df-rmo 3344  df-reu 3345

This theorem is referenced by:  2reu2rex  3356  reu3  3668  reuxfr1d  3691  2rexreu  3703  sbcreu  3808  reu0  4289  2reu4  4452  weniso  7298  oawordex  8482  oaabs  8574  oaabs2  8575  supval2  9358  fisup2g  9372  fiinf2g  9405  nqerf  10844  qbtwnre  13142  modprm0  16767  issrgid  20176  isringid  20243  isringrng  20259  lspsneu  21116  frgpcyg  21548  qtophmeo  23800  pjthlem2  25423  dyadmax  25583  quotlem  26284  2sqreulem1  27427  2sqreunnlem1  27430  nfrgr2v  30360  2pthfrgrrn  30370  frgrncvvdeqlem9  30395  frgr2wwlkn0  30416  pjhthlem2  31481  cnlnadj  32168  2reu2rex1  32568  rmoxfrd  32580  cvmliftpht  35546  finorwe  37744  lcfl7N  41993  renegeulem  42846  resubeqsub  42907  requad1  48113  requad2  48114  uzlidlring  48726  reuxfr1dd  49297  lubeldm2  49446  glbeldm2  49447  upciclem4  49659