Theorem reurex 3347

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

Syntax hints:   → wi 4  ∃wrex 3053  ∃!wreu 3341  ∃*wrmo 3342

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 2562  df-rex 3054  df-rmo 3343  df-reu 3344

This theorem is referenced by:  2reu2rex  3357  reu3  3687  reuxfr1d  3710  2rexreu  3722  sbcreu  3828  reu0  4312  2reu4  4474  weniso  7291  oawordex  8475  oaabs  8566  oaabs2  8567  supval2  9345  fisup2g  9359  fiinf2g  9392  nqerf  10824  qbtwnre  13101  modprm0  16717  issrgid  20089  isringid  20156  isringrng  20172  lspsneu  21030  frgpcyg  21480  qtophmeo  23702  pjthlem2  25336  dyadmax  25497  quotlem  26206  2sqreulem1  27355  2sqreunnlem1  27358  nfrgr2v  30216  2pthfrgrrn  30226  frgrncvvdeqlem9  30251  frgr2wwlkn0  30272  pjhthlem2  31336  cnlnadj  32023  2reu2rex1  32425  rmoxfrd  32437  cvmliftpht  35295  finorwe  37360  lcfl7N  41484  renegeulem  42346  resubeqsub  42407  requad1  47610  requad2  47611  uzlidlring  48223  reuxfr1dd  48795  lubeldm2  48944  glbeldm2  48945  upciclem4  49158