Theorem reurex 3360

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

Syntax hints:   → wi 4  ∃wrex 3054  ∃!wreu 3354  ∃*wrmo 3355

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 2563  df-rex 3055  df-rmo 3356  df-reu 3357

This theorem is referenced by:  2reu2rex  3370  reu3  3701  reuxfr1d  3724  2rexreu  3736  sbcreu  3842  reu0  4327  2reu4  4489  weniso  7332  oawordex  8524  oaabs  8615  oaabs2  8616  supval2  9413  fisup2g  9427  fiinf2g  9460  nqerf  10890  qbtwnre  13166  modprm0  16783  issrgid  20120  isringid  20187  isringrng  20203  lspsneu  21040  frgpcyg  21490  qtophmeo  23711  pjthlem2  25345  dyadmax  25506  quotlem  26215  2sqreulem1  27364  2sqreunnlem1  27367  nfrgr2v  30208  2pthfrgrrn  30218  frgrncvvdeqlem9  30243  frgr2wwlkn0  30264  pjhthlem2  31328  cnlnadj  32015  2reu2rex1  32417  rmoxfrd  32429  cvmliftpht  35312  finorwe  37377  lcfl7N  41502  renegeulem  42364  resubeqsub  42425  requad1  47627  requad2  47628  uzlidlring  48227  reuxfr1dd  48799  lubeldm2  48948  glbeldm2  48949  upciclem4  49162