Theorem reurex 3358

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

Syntax hints:   → wi 4  ∃wrex 3053  ∃!wreu 3352  ∃*wrmo 3353

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 2562  df-rex 3054  df-rmo 3354  df-reu 3355

This theorem is referenced by:  2reu2rex  3368  reu3  3698  reuxfr1d  3721  2rexreu  3733  sbcreu  3839  reu0  4324  2reu4  4486  weniso  7329  oawordex  8521  oaabs  8612  oaabs2  8613  supval2  9406  fisup2g  9420  fiinf2g  9453  nqerf  10883  qbtwnre  13159  modprm0  16776  issrgid  20113  isringid  20180  isringrng  20196  lspsneu  21033  frgpcyg  21483  qtophmeo  23704  pjthlem2  25338  dyadmax  25499  quotlem  26208  2sqreulem1  27357  2sqreunnlem1  27360  nfrgr2v  30201  2pthfrgrrn  30211  frgrncvvdeqlem9  30236  frgr2wwlkn0  30257  pjhthlem2  31321  cnlnadj  32008  2reu2rex1  32410  rmoxfrd  32422  cvmliftpht  35305  finorwe  37370  lcfl7N  41495  renegeulem  42357  resubeqsub  42418  requad1  47623  requad2  47624  uzlidlring  48223  reuxfr1dd  48795  lubeldm2  48944  glbeldm2  48945  upciclem4  49158