Theorem reurex 3373

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

Syntax hints:   → wi 4  ∃wrex 3089  ∃!wreu 3367  ∃*wrmo 3368

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 210  df-an 401  df-eu 2597  df-rex 3090  df-rmo 3369  df-reu 3370

This theorem is referenced by:  2reu2rex  3381  reu3  3691  reuxfr1d  3714  2rexreu  3726  sbcreu  3830  reu0  4317  2reu4  4486  weniso  7354  oawordex  8543  oaabs  8635  oaabs2  8636  supval2  9416  fisup2g  9430  fiinf2g  9463  nqerf  10916  qbtwnre  13226  modprm0  16866  issrgid  20287  isringid  20355  isringrng  20371  lspsneu  21228  frgpcyg  21704  qtophmeo  23955  pjthlem2  25578  dyadmax  25738  quotlem  26442  2sqreulem1  27588  2sqreunnlem1  27591  nfrgr2v  30601  2pthfrgrrn  30611  frgrncvvdeqlem9  30636  frgr2wwlkn0  30657  pjhthlem2  31722  cnlnadj  32409  2reu2rex1  32805  rmoxfrd  32817  cvmliftpht  35788  finorwe  38006  lcfl7N  42253  renegeulem  43108  resubeqsub  43169  requad1  48364  requad2  48365  uzlidlring  48977  reuxfr1dd  49562  lubeldm2  49711  glbeldm2  49712  upciclem4  49924