Theorem reurex 3371

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3088  ∃!wreu 3365  ∃*wrmo 3366

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 2596  df-rex 3089  df-rmo 3367  df-reu 3368

This theorem is used by:  2reu2rex  3379  reu3  3688  reuxfr1d  3711  2rexreu  3723  sbcreu  3826  reu0  4312  2reu4  4483  weniso  7361  oawordex  8548  oaabs  8640  oaabs2  8641  supval2  9429  fisup2g  9443  fiinf2g  9476  nqerf  10943  qbtwnre  13255  modprm0  16903  issrgid  20349  isringid  20418  isringrng  20434  lspsneu  21316  frgpcyg  21792  qtophmeo  24049  pjthlem2  25672  dyadmax  25832  quotlem  26537  2sqreulem1  27690  2sqreunnlem1  27693  angmgmaddcpbl  29277  angmgmaddcl  29278  nfrgr2v  30760  2pthfrgrrn  30770  frgrncvvdeqlem9  30795  frgr2wwlkn0  30816  pjhthlem2  31881  cnlnadj  32568  2reu2rex1  32964  rmoxfrd  32976  cvmliftpht  35905  finorwe  38144  lcfl7N  42382  renegeulem  43252  resubeqsub  43313  requad1  48546  requad2  48547  uzlidlring  49158  reuxfr1dd  49743  lubeldm2  49890  glbeldm2  49891  upciclem4  50103  ralseurals  50762