Theorem reurex 3355

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

Syntax hints:   → wi 4  ∃wrex 3069  ∃!wreu 3349  ∃*wrmo 3350

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 397  df-eu 2562  df-rex 3070  df-rmo 3351  df-reu 3352

This theorem is referenced by:  2reu2rex  3365  reu3  3688  reuxfr1d  3711  2rexreu  3723  sbcreu  3835  reu0  4323  2reu4  4489  tz6.26OLD  6307  weniso  7304  oawordex  8509  oaabs  8599  oaabs2  8600  supval2  9400  fisup2g  9413  fiinf2g  9445  nqerf  10875  qbtwnre  13128  modprm0  16688  issrgid  19949  isringid  20008  lspsneu  20643  frgpcyg  21017  qtophmeo  23205  pjthlem2  24839  dyadmax  24999  quotlem  25697  2sqreulem1  26831  2sqreunnlem1  26834  nfrgr2v  29279  2pthfrgrrn  29289  frgrncvvdeqlem9  29314  frgr2wwlkn0  29335  pjhthlem2  30397  cnlnadj  31084  2reu2rex1  31473  rmoxfrd  31485  cvmliftpht  33999  finorwe  35926  lcfl7N  40037  renegeulem  40896  resubeqsub  40956  requad1  45934  requad2  45935  isringrng  46299  uzlidlring  46347  lubeldm2  47109  glbeldm2  47110