Theorem reurex 3137

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

Syntax hints:   → wi 4  ∃wrex 2897  ∃!wreu 2898  ∃*wrmo 2899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-eu 2462  df-mo 2463  df-rex 2902  df-reu 2903  df-rmo 2904

This theorem is referenced by:  reu3  3363  sbcreu  3482  reuxfrd  4819  tz6.26  5628  weniso  6504  oawordex  7524  oaabs  7611  oaabs2  7612  supval2  8244  fisup2g  8257  fiinf2g  8289  nqerf  9631  qbtwnre  11904  modprm0  15348  meet0  16960  join0  16961  issrgid  18346  isringid  18396  lspsneu  18944  frgpcyg  19741  qtophmeo  21430  pjthlem2  23017  dyadmax  23172  quotlem  23859  frgra2v  26526  2pthfrgrarn  26536  frgrancvvdeqlemC  26566  frg2wotn0  26583  pjhthlem2  27635  cnlnadj  28322  reuxfr4d  28714  rmoxfrdOLD  28716  rmoxfrd  28717  cvmliftpht  30554  lcfl7N  35808  2reu2rex  39832  2rexreu  39834  2reu4  39839  nfrgr2v  41442  2pthfrgrrn  41452  frgrncvvdeqlemC  41478  frgr2wwlkn0  41493  isringrng  41671  uzlidlring  41719