Theorem reurex 3362

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 498	1 ⊢ (∃!𝑥 ∈ 𝐴 𝜑 → ∃𝑥 ∈ 𝐴 𝜑)

Syntax hints:   → wi 4  ∃wrex 3065  ∃!wreu 3066  ∃*wrmo 3067

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 206  df-an 397  df-eu 2569  df-rex 3070  df-rmo 3071  df-reu 3072

This theorem is referenced by:  2reu2rex  3363  reu3  3662  reuxfr1d  3685  2rexreu  3697  sbcreu  3809  reu0  4292  2reu4  4457  tz6.26OLD  6251  weniso  7225  oawordex  8388  oaabs  8478  oaabs2  8479  supval2  9214  fisup2g  9227  fiinf2g  9259  nqerf  10686  qbtwnre  12933  modprm0  16506  issrgid  19759  isringid  19812  lspsneu  20385  frgpcyg  20781  qtophmeo  22968  pjthlem2  24602  dyadmax  24762  quotlem  25460  2sqreulem1  26594  2sqreunnlem1  26597  nfrgr2v  28636  2pthfrgrrn  28646  frgrncvvdeqlem9  28671  frgr2wwlkn0  28692  pjhthlem2  29754  cnlnadj  30441  2reu2rex1  30829  rmoxfrd  30841  cvmliftpht  33280  finorwe  35553  lcfl7N  39515  renegeulem  40352  resubeqsub  40411  requad1  45074  requad2  45075  isringrng  45439  uzlidlring  45487  lubeldm2  46250  glbeldm2  46251