Theorem reurex 3392

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

Syntax hints:   → wi 4  ∃wrex 3076  ∃!wreu 3386  ∃*wrmo 3387

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 2572  df-rex 3077  df-rmo 3388  df-reu 3389

This theorem is referenced by:  2reu2rex  3402  reu3  3749  reuxfr1d  3772  2rexreu  3784  sbcreu  3898  reu0  4384  2reu4  4546  tz6.26OLD  6380  weniso  7390  oawordex  8613  oaabs  8704  oaabs2  8705  supval2  9524  fisup2g  9537  fiinf2g  9569  nqerf  10999  qbtwnre  13261  modprm0  16852  issrgid  20231  isringid  20294  isringrng  20310  lspsneu  21148  frgpcyg  21615  qtophmeo  23846  pjthlem2  25491  dyadmax  25652  quotlem  26360  2sqreulem1  27508  2sqreunnlem1  27511  nfrgr2v  30304  2pthfrgrrn  30314  frgrncvvdeqlem9  30339  frgr2wwlkn0  30360  pjhthlem2  31424  cnlnadj  32111  2reu2rex1  32509  rmoxfrd  32521  cvmliftpht  35286  finorwe  37348  lcfl7N  41458  renegeulem  42345  resubeqsub  42405  requad1  47496  requad2  47497  uzlidlring  47958  lubeldm2  48636  glbeldm2  48637