Theorem reurex 3350

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

Syntax hints:   → wi 4  ∃wrex 3056  ∃!wreu 3344  ∃*wrmo 3345

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 207  df-an 396  df-eu 2564  df-rex 3057  df-rmo 3346  df-reu 3347

This theorem is referenced by:  2reu2rex  3358  reu3  3686  reuxfr1d  3709  2rexreu  3721  sbcreu  3827  reu0  4311  2reu4  4473  weniso  7288  oawordex  8472  oaabs  8563  oaabs2  8564  supval2  9339  fisup2g  9353  fiinf2g  9386  nqerf  10818  qbtwnre  13095  modprm0  16714  issrgid  20120  isringid  20187  isringrng  20203  lspsneu  21058  frgpcyg  21508  qtophmeo  23730  pjthlem2  25363  dyadmax  25524  quotlem  26233  2sqreulem1  27382  2sqreunnlem1  27385  nfrgr2v  30247  2pthfrgrrn  30257  frgrncvvdeqlem9  30282  frgr2wwlkn0  30303  pjhthlem2  31367  cnlnadj  32054  2reu2rex1  32455  rmoxfrd  32467  cvmliftpht  35350  finorwe  37415  lcfl7N  41539  renegeulem  42401  resubeqsub  42462  requad1  47652  requad2  47653  uzlidlring  48265  reuxfr1dd  48837  lubeldm2  48986  glbeldm2  48987  upciclem4  49200