Theorem reurex 3369

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

This proof depends on syntax axioms:   → wi 4  ∃wrex 3086  ∃!wreu 3363  ∃*wrmo 3364

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 2594  df-rex 3087  df-rmo 3365  df-reu 3366

This theorem is used by:  2reu2rex  3377  reu3  3684  reuxfr1d  3707  2rexreu  3719  sbcreu  3822  reu0  4308  2reu4  4479  weniso  7364  oawordex  8568  oaabs  8660  oaabs2  8661  supval2  9450  fisup2g  9464  fiinf2g  9497  nqerf  11018  qbtwnre  13332  modprm0  16988  issrgid  20435  isringid  20505  isringrng  20521  lspsneu  21406  frgpcyg  21884  qtophmeo  24141  pjthlem2  25764  dyadmax  25924  quotlem  26626  2sqreulem1  27778  2sqreunnlem1  27781  angmgmaddcpbl  29395  angmgmaddcl  29396  nfrgr2v  30878  2pthfrgrrn  30888  frgrncvvdeqlem9  30913  frgr2wwlkn0  30934  pjhthlem2  31999  cnlnadj  32686  2reu2rex1  33124  rmoxfrd  33136  cvmliftpht  36169  finorwe  38398  lcfl7N  42651  renegeulem  43513  resubeqsub  43574  requad1  48813  requad2  48814  uzlidlring  49425  reuxfr1dd  50010  lubeldm2  50163  glbeldm2  50164  upciclem4  50378  ralseurals  51089