Theorem reurex 3354

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

Syntax hints:   → wi 4  ∃wrex 3060  ∃!wreu 3348  ∃*wrmo 3349

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 2569  df-rex 3061  df-rmo 3350  df-reu 3351

This theorem is referenced by:  2reu2rex  3362  reu3  3685  reuxfr1d  3708  2rexreu  3720  sbcreu  3826  reu0  4313  2reu4  4477  weniso  7300  oawordex  8484  oaabs  8576  oaabs2  8577  supval2  9358  fisup2g  9372  fiinf2g  9405  nqerf  10841  qbtwnre  13114  modprm0  16733  issrgid  20139  isringid  20206  isringrng  20222  lspsneu  21078  frgpcyg  21528  qtophmeo  23761  pjthlem2  25394  dyadmax  25555  quotlem  26264  2sqreulem1  27413  2sqreunnlem1  27416  nfrgr2v  30347  2pthfrgrrn  30357  frgrncvvdeqlem9  30382  frgr2wwlkn0  30403  pjhthlem2  31467  cnlnadj  32154  2reu2rex1  32555  rmoxfrd  32567  cvmliftpht  35512  finorwe  37583  lcfl7N  41757  renegeulem  42620  resubeqsub  42681  requad1  47864  requad2  47865  uzlidlring  48477  reuxfr1dd  49048  lubeldm2  49197  glbeldm2  49198  upciclem4  49410