Theorem reurex 3349

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

Syntax hints:   → wi 4  ∃wrex 3064  ∃!wreu 3343  ∃*wrmo 3344

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 208  df-an 397  df-eu 2573  df-rex 3065  df-rmo 3345  df-reu 3346

This theorem is referenced by:  2reu2rex  3357  reu3  3675  reuxfr1d  3698  2rexreu  3710  sbcreu  3815  reu0  4296  2reu4  4459  weniso  7305  oawordex  8489  oaabs  8581  oaabs2  8582  supval2  9365  fisup2g  9379  fiinf2g  9412  nqerf  10851  qbtwnre  13149  modprm0  16774  issrgid  20183  isringid  20250  isringrng  20266  lspsneu  21123  frgpcyg  21555  qtophmeo  23807  pjthlem2  25430  dyadmax  25590  quotlem  26291  2sqreulem1  27434  2sqreunnlem1  27437  nfrgr2v  30367  2pthfrgrrn  30377  frgrncvvdeqlem9  30402  frgr2wwlkn0  30423  pjhthlem2  31488  cnlnadj  32175  2reu2rex1  32575  rmoxfrd  32587  cvmliftpht  35553  finorwe  37751  lcfl7N  42000  renegeulem  42853  resubeqsub  42914  requad1  48120  requad2  48121  uzlidlring  48733  reuxfr1dd  49304  lubeldm2  49453  glbeldm2  49454  upciclem4  49666