Theorem reurex 3360

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

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

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 396  df-eu 2570  df-rex 3071  df-reu 3072  df-rmo 3073

This theorem is referenced by:  2reu2rex  3361  reu3  3665  reuxfr1d  3688  2rexreu  3700  sbcreu  3813  reu0  4297  2reu4  4462  tz6.26OLD  6248  weniso  7218  oawordex  8364  oaabs  8452  oaabs2  8453  supval2  9175  fisup2g  9188  fiinf2g  9220  nqerf  10670  qbtwnre  12915  modprm0  16487  issrgid  19740  isringid  19793  lspsneu  20366  frgpcyg  20762  qtophmeo  22949  pjthlem2  24583  dyadmax  24743  quotlem  25441  2sqreulem1  26575  2sqreunnlem1  26578  nfrgr2v  28615  2pthfrgrrn  28625  frgrncvvdeqlem9  28650  frgr2wwlkn0  28671  pjhthlem2  29733  cnlnadj  30420  2reu2rex1  30808  rmoxfrd  30820  cvmliftpht  33259  finorwe  35532  lcfl7N  39494  renegeulem  40332  resubeqsub  40391  requad1  45026  requad2  45027  isringrng  45391  uzlidlring  45439  lubeldm2  46202  glbeldm2  46203