Theorem reurex 3349

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

Syntax hints:   → wi 4  ∃wrex 3053  ∃!wreu 3343  ∃*wrmo 3344

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 2562  df-rex 3054  df-rmo 3345  df-reu 3346

This theorem is referenced by:  2reu2rex  3359  reu3  3689  reuxfr1d  3712  2rexreu  3724  sbcreu  3830  reu0  4314  2reu4  4476  weniso  7295  oawordex  8482  oaabs  8573  oaabs2  8574  supval2  9364  fisup2g  9378  fiinf2g  9411  nqerf  10843  qbtwnre  13119  modprm0  16735  issrgid  20107  isringid  20174  isringrng  20190  lspsneu  21048  frgpcyg  21498  qtophmeo  23720  pjthlem2  25354  dyadmax  25515  quotlem  26224  2sqreulem1  27373  2sqreunnlem1  27376  nfrgr2v  30234  2pthfrgrrn  30244  frgrncvvdeqlem9  30269  frgr2wwlkn0  30290  pjhthlem2  31354  cnlnadj  32041  2reu2rex1  32443  rmoxfrd  32455  cvmliftpht  35290  finorwe  37355  lcfl7N  41480  renegeulem  42342  resubeqsub  42403  requad1  47607  requad2  47608  uzlidlring  48220  reuxfr1dd  48792  lubeldm2  48941  glbeldm2  48942  upciclem4  49155