Theorem reurex 3363

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

Syntax hints:   → wi 4  ∃wrex 3060  ∃!wreu 3357  ∃*wrmo 3358

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 2568  df-rex 3061  df-rmo 3359  df-reu 3360

This theorem is referenced by:  2reu2rex  3373  reu3  3710  reuxfr1d  3733  2rexreu  3745  sbcreu  3851  reu0  4336  2reu4  4498  tz6.26OLD  6337  weniso  7347  oawordex  8569  oaabs  8660  oaabs2  8661  supval2  9467  fisup2g  9481  fiinf2g  9514  nqerf  10944  qbtwnre  13215  modprm0  16825  issrgid  20164  isringid  20231  isringrng  20247  lspsneu  21084  frgpcyg  21534  qtophmeo  23755  pjthlem2  25390  dyadmax  25551  quotlem  26260  2sqreulem1  27409  2sqreunnlem1  27412  nfrgr2v  30253  2pthfrgrrn  30263  frgrncvvdeqlem9  30288  frgr2wwlkn0  30309  pjhthlem2  31373  cnlnadj  32060  2reu2rex1  32462  rmoxfrd  32474  cvmliftpht  35340  finorwe  37400  lcfl7N  41520  renegeulem  42412  resubeqsub  42472  requad1  47636  requad2  47637  uzlidlring  48210  reuxfr1dd  48785  lubeldm2  48930  glbeldm2  48931  upciclem4  49104