Theorem reurex 3373

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3090  ∃!wreu 3367  ∃*wrmo 3368

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 2597  df-rex 3091  df-rmo 3369  df-reu 3370

This theorem is used by:  2reu2rex  3381  reu3  3688  reuxfr1d  3711  2rexreu  3723  sbcreu  3827  reu0  4312  2reu4  4483  weniso  7387  oawordex  8593  oaabs  8685  oaabs2  8686  supval2  9474  fisup2g  9488  fiinf2g  9521  nqerf  11042  qbtwnre  13356  modprm0  17012  issrgid  20460  isringid  20530  isringrng  20546  lspsneu  21431  frgpcyg  21909  qtophmeo  24166  pjthlem2  25789  dyadmax  25949  quotlem  26651  2sqreulem1  27803  2sqreunnlem1  27806  angmgmaddcpbl  29420  angmgmaddcl  29421  nfrgr2v  30903  2pthfrgrrn  30913  frgrncvvdeqlem9  30938  frgr2wwlkn0  30959  pjhthlem2  32024  cnlnadj  32711  2reu2rex1  33149  rmoxfrd  33161  cvmliftpht  36250  finorwe  38497  lcfl7N  42750  renegeulem  43613  resubeqsub  43674  requad1  48925  requad2  48926  uzlidlring  49537  reuxfr1dd  50122  lubeldm2  50275  glbeldm2  50276  upciclem4  50490  ralseurals  51201