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

Syntax hints:   → wi 4  ∃wrex 3107  ∃!wreu 3108  ∃*wrmo 3109

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 210  df-an 400  df-eu 2629  df-rex 3112  df-reu 3113  df-rmo 3114

This theorem is referenced by:  2reu2rex  3377  reu3  3666  reuxfr1d  3689  2rexreu  3701  sbcreu  3805  reu0  4272  2reu4  4424  tz6.26  6147  weniso  7086  oawordex  8166  oaabs  8254  oaabs2  8255  supval2  8903  fisup2g  8916  fiinf2g  8948  nqerf  10341  qbtwnre  12580  modprm0  16132  issrgid  19266  isringid  19319  lspsneu  19888  frgpcyg  20265  qtophmeo  22422  pjthlem2  24042  dyadmax  24202  quotlem  24896  2sqreulem1  26030  2sqreunnlem1  26033  nfrgr2v  28057  2pthfrgrrn  28067  frgrncvvdeqlem9  28092  frgr2wwlkn0  28113  pjhthlem2  29175  cnlnadj  29862  2reu2rex1  30251  rmoxfrd  30264  cvmliftpht  32678  finorwe  34799  lcfl7N  38797  renegeulem  39507  resubeqsub  39566  requad1  44140  requad2  44141  isringrng  44505  uzlidlring  44553