Theorem reurex 3160

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

Syntax hints:   → wi 4  ∃wrex 2913  ∃!wreu 2914  ∃*wrmo 2915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-eu 2474  df-mo 2475  df-rex 2918  df-reu 2919  df-rmo 2920

This theorem is referenced by:  reu3  3396  sbcreu  3515  reuxfrd  4893  tz6.26  5711  weniso  6604  oawordex  7637  oaabs  7724  oaabs2  7725  supval2  8361  fisup2g  8374  fiinf2g  8406  nqerf  9752  qbtwnre  12030  modprm0  15510  meet0  17137  join0  17138  issrgid  18523  isringid  18573  lspsneu  19123  frgpcyg  19922  qtophmeo  21620  pjthlem2  23209  dyadmax  23366  quotlem  24055  nfrgr2v  27136  2pthfrgrrn  27146  frgrncvvdeqlem9  27171  frgr2wwlkn0  27192  pjhthlem2  28251  cnlnadj  28938  reuxfr4d  29330  rmoxfrdOLD  29332  rmoxfrd  29333  cvmliftpht  31300  lcfl7N  36790  2reu2rex  41183  2rexreu  41185  2reu4  41190  isringrng  41881  uzlidlring  41929