Theorem reurex 3352

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

Syntax hints:   → wi 4  ∃wrex 3064  ∃!wreu 3065  ∃*wrmo 3066

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 206  df-an 396  df-eu 2569  df-rex 3069  df-reu 3070  df-rmo 3071

This theorem is referenced by:  2reu2rex  3353  reu3  3657  reuxfr1d  3680  2rexreu  3692  sbcreu  3805  reu0  4289  2reu4  4454  tz6.26OLD  6236  weniso  7205  oawordex  8350  oaabs  8438  oaabs2  8439  supval2  9144  fisup2g  9157  fiinf2g  9189  nqerf  10617  qbtwnre  12862  modprm0  16434  issrgid  19674  isringid  19727  lspsneu  20300  frgpcyg  20693  qtophmeo  22876  pjthlem2  24507  dyadmax  24667  quotlem  25365  2sqreulem1  26499  2sqreunnlem1  26502  nfrgr2v  28537  2pthfrgrrn  28547  frgrncvvdeqlem9  28572  frgr2wwlkn0  28593  pjhthlem2  29655  cnlnadj  30342  2reu2rex1  30730  rmoxfrd  30742  cvmliftpht  33180  finorwe  35480  lcfl7N  39442  renegeulem  40273  resubeqsub  40332  requad1  44962  requad2  44963  isringrng  45327  uzlidlring  45375  lubeldm2  46138  glbeldm2  46139