Theorem reurex 3368

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

Syntax hints:   → wi 4  ∃wrex 3060  ∃!wreu 3362  ∃*wrmo 3363

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 2558  df-rex 3061  df-rmo 3364  df-reu 3365

This theorem is referenced by:  2reu2rex  3378  reu3  3720  reuxfr1d  3743  2rexreu  3755  sbcreu  3868  reu0  4354  2reu4  4521  tz6.26OLD  6353  weniso  7358  oawordex  8579  oaabs  8670  oaabs2  8671  supval2  9491  fisup2g  9504  fiinf2g  9536  nqerf  10964  qbtwnre  13226  modprm0  16802  issrgid  20183  isringid  20246  isringrng  20262  lspsneu  21100  frgpcyg  21567  qtophmeo  23809  pjthlem2  25454  dyadmax  25615  quotlem  26325  2sqreulem1  27472  2sqreunnlem1  27475  nfrgr2v  30202  2pthfrgrrn  30212  frgrncvvdeqlem9  30237  frgr2wwlkn0  30258  pjhthlem2  31322  cnlnadj  32009  2reu2rex1  32406  rmoxfrd  32418  cvmliftpht  35159  finorwe  37102  lcfl7N  41213  renegeulem  42080  resubeqsub  42140  requad1  47230  requad2  47231  uzlidlring  47648  lubeldm2  48326  glbeldm2  48327