Theorem reurex 3347

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

Syntax hints:   → wi 4  ∃wrex 3062  ∃!wreu 3341  ∃*wrmo 3342

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 2570  df-rex 3063  df-rmo 3343  df-reu 3344

This theorem is referenced by:  2reu2rex  3355  reu3  3674  reuxfr1d  3697  2rexreu  3709  sbcreu  3815  reu0  4302  2reu4  4465  weniso  7302  oawordex  8485  oaabs  8577  oaabs2  8578  supval2  9361  fisup2g  9375  fiinf2g  9408  nqerf  10844  qbtwnre  13142  modprm0  16767  issrgid  20176  isringid  20243  isringrng  20259  lspsneu  21113  frgpcyg  21563  qtophmeo  23792  pjthlem2  25415  dyadmax  25575  quotlem  26277  2sqreulem1  27423  2sqreunnlem1  27426  nfrgr2v  30357  2pthfrgrrn  30367  frgrncvvdeqlem9  30392  frgr2wwlkn0  30413  pjhthlem2  31478  cnlnadj  32165  2reu2rex1  32565  rmoxfrd  32577  cvmliftpht  35516  finorwe  37712  lcfl7N  41961  renegeulem  42815  resubeqsub  42876  requad1  48110  requad2  48111  uzlidlring  48723  reuxfr1dd  49294  lubeldm2  49443  glbeldm2  49444  upciclem4  49656