Theorem reurex 3431

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

Syntax hints:   → wi 4  ∃wrex 3139  ∃!wreu 3140  ∃*wrmo 3141

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 209  df-an 399  df-eu 2654  df-rex 3144  df-reu 3145  df-rmo 3146

This theorem is referenced by:  2reu2rex  3432  reu3  3718  reuxfr1d  3741  2rexreu  3753  sbcreu  3859  reu0  4318  2reu4  4466  tz6.26  6179  weniso  7107  oawordex  8183  oaabs  8271  oaabs2  8272  supval2  8919  fisup2g  8932  fiinf2g  8964  nqerf  10352  qbtwnre  12593  modprm0  16142  issrgid  19273  isringid  19323  lspsneu  19895  frgpcyg  20720  qtophmeo  22425  pjthlem2  24041  dyadmax  24199  quotlem  24889  2sqreulem1  26022  2sqreunnlem1  26025  nfrgr2v  28051  2pthfrgrrn  28061  frgrncvvdeqlem9  28086  frgr2wwlkn0  28107  pjhthlem2  29169  cnlnadj  29856  2reu2rex1  30244  rmoxfrd  30257  cvmliftpht  32565  finorwe  34666  lcfl7N  38652  renegeulem  39219  requad1  43807  requad2  43808  isringrng  44172  uzlidlring  44220