Theorem reurex 3382

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

Syntax hints:   → wi 4  ∃wrex 3068  ∃!wreu 3376  ∃*wrmo 3377

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 2567  df-rex 3069  df-rmo 3378  df-reu 3379

This theorem is referenced by:  2reu2rex  3392  reu3  3736  reuxfr1d  3759  2rexreu  3771  sbcreu  3885  reu0  4367  2reu4  4529  tz6.26OLD  6371  weniso  7374  oawordex  8594  oaabs  8685  oaabs2  8686  supval2  9493  fisup2g  9506  fiinf2g  9538  nqerf  10968  qbtwnre  13238  modprm0  16839  issrgid  20222  isringid  20285  isringrng  20301  lspsneu  21143  frgpcyg  21610  qtophmeo  23841  pjthlem2  25486  dyadmax  25647  quotlem  26357  2sqreulem1  27505  2sqreunnlem1  27508  nfrgr2v  30301  2pthfrgrrn  30311  frgrncvvdeqlem9  30336  frgr2wwlkn0  30357  pjhthlem2  31421  cnlnadj  32108  2reu2rex1  32509  rmoxfrd  32521  cvmliftpht  35303  finorwe  37365  lcfl7N  41484  renegeulem  42376  resubeqsub  42436  requad1  47547  requad2  47548  uzlidlring  48079  reuxfr1dd  48655  lubeldm2  48753  glbeldm2  48754  upciclem4  48815