Theorem reurex 3378

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

Syntax hints:   → wi 4  ∃wrex 3068  ∃!wreu 3372  ∃*wrmo 3373

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 395  df-eu 2561  df-rex 3069  df-rmo 3374  df-reu 3375

This theorem is referenced by:  2reu2rex  3388  reu3  3724  reuxfr1d  3747  2rexreu  3759  sbcreu  3871  reu0  4359  2reu4  4527  tz6.26OLD  6350  weniso  7355  oawordex  8561  oaabs  8651  oaabs2  8652  supval2  9454  fisup2g  9467  fiinf2g  9499  nqerf  10929  qbtwnre  13184  modprm0  16744  issrgid  20100  isringid  20161  isringrng  20177  lspsneu  20883  frgpcyg  21350  qtophmeo  23543  pjthlem2  25188  dyadmax  25349  quotlem  26047  2sqreulem1  27183  2sqreunnlem1  27186  nfrgr2v  29790  2pthfrgrrn  29800  frgrncvvdeqlem9  29825  frgr2wwlkn0  29846  pjhthlem2  30910  cnlnadj  31597  2reu2rex1  31986  rmoxfrd  31998  cvmliftpht  34605  finorwe  36568  lcfl7N  40677  renegeulem  41546  resubeqsub  41606  requad1  46590  requad2  46591  uzlidlring  46917  lubeldm2  47678  glbeldm2  47679