Theorem reurex 3384

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

Syntax hints:   → wi 4  ∃wrex 3070  ∃!wreu 3378  ∃*wrmo 3379

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 2569  df-rex 3071  df-rmo 3380  df-reu 3381

This theorem is referenced by:  2reu2rex  3394  reu3  3733  reuxfr1d  3756  2rexreu  3768  sbcreu  3876  reu0  4361  2reu4  4523  tz6.26OLD  6369  weniso  7374  oawordex  8595  oaabs  8686  oaabs2  8687  supval2  9495  fisup2g  9508  fiinf2g  9540  nqerf  10970  qbtwnre  13241  modprm0  16843  issrgid  20201  isringid  20268  isringrng  20284  lspsneu  21125  frgpcyg  21592  qtophmeo  23825  pjthlem2  25472  dyadmax  25633  quotlem  26342  2sqreulem1  27490  2sqreunnlem1  27493  nfrgr2v  30291  2pthfrgrrn  30301  frgrncvvdeqlem9  30326  frgr2wwlkn0  30347  pjhthlem2  31411  cnlnadj  32098  2reu2rex1  32500  rmoxfrd  32512  cvmliftpht  35323  finorwe  37383  lcfl7N  41503  renegeulem  42399  resubeqsub  42459  requad1  47609  requad2  47610  uzlidlring  48151  reuxfr1dd  48726  lubeldm2  48853  glbeldm2  48854  upciclem4  48926