Theorem reurex 3371

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

Syntax hints:   → wi 4  ∃wrex 3089  ∃!wreu 3090  ∃*wrmo 3091

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 199  df-an 388  df-eu 2583  df-rex 3094  df-reu 3095  df-rmo 3096

This theorem is referenced by:  2reu2rex  3372  reu3  3632  reuxfr4d  3654  2rexreu  3664  sbcreu  3764  reu0  4206  2reu4  4350  reuxfrd  5175  tz6.26  6019  weniso  6932  oawordex  7986  oaabs  8073  oaabs2  8074  supval2  8716  fisup2g  8729  fiinf2g  8761  nqerf  10152  qbtwnre  12412  modprm0  16001  issrgid  18999  isringid  19049  lspsneu  19620  frgpcyg  20425  qtophmeo  22132  pjthlem2  23747  dyadmax  23905  quotlem  24595  2sqreulem1  25727  2sqreunnlem1  25730  nfrgr2v  27809  2pthfrgrrn  27819  frgrncvvdeqlem9  27844  frgr2wwlkn0  27865  pjhthlem2  28953  cnlnadj  29640  2reu2rex1  30029  rmoxfrd  30041  cvmliftpht  32150  lcfl7N  38082  renegeulem  38631  requad1  43156  requad2  43157  isringrng  43517  uzlidlring  43565