Theorem reurex 3376

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3092  ∃!wreu 3370  ∃*wrmo 3371

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2600  df-rex 3093  df-rmo 3372  df-reu 3373

This theorem is used by:  2reu2rex  3384  reu3  3693  reuxfr1d  3716  2rexreu  3728  sbcreu  3832  reu0  4319  2reu4  4490  weniso  7365  oawordex  8551  oaabs  8643  oaabs2  8644  supval2  9425  fisup2g  9439  fiinf2g  9472  nqerf  10933  qbtwnre  13243  modprm0  16890  issrgid  20317  isringid  20386  isringrng  20402  lspsneu  21284  frgpcyg  21760  qtophmeo  24011  pjthlem2  25634  dyadmax  25794  quotlem  26498  2sqreulem1  27647  2sqreunnlem1  27650  nfrgr2v  30660  2pthfrgrrn  30670  frgrncvvdeqlem9  30695  frgr2wwlkn0  30716  pjhthlem2  31781  cnlnadj  32468  2reu2rex1  32864  rmoxfrd  32876  cvmliftpht  35831  finorwe  38069  lcfl7N  42316  renegeulem  43171  resubeqsub  43232  requad1  48428  requad2  48429  uzlidlring  49041  reuxfr1dd  49626  lubeldm2  49775  glbeldm2  49776  upciclem4  49988  ralseurals  50644