Theorem euex 2605

Description: Existential uniqueness implies existence. (Contributed by NM, 15-Sep-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.) (Proof shortened by Wolf Lammen, 4-Dec-2018.) (Proof shortened by BJ, 7-Oct-2022.)

Assertion

Ref	Expression
euex	⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Proof of Theorem euex

Step	Hyp	Ref	Expression
1		df-eu 2597	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2	1	simplbi 502	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∃wex 1811  ∃*wmo 2565  ∃!weu 2596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2597

This theorem is used by:  exmoeu  2609  dfeu  2623  euan  2649  euanv  2652  2exeuv  2660  eupickbi  2664  2eu2ex  2671  2exeu  2674  euxfrw  3682  euxfr  3684  zfrep6  5245  eusvnf  5358  eusvnfb  5359  reusv2lem2  5365  reusv2lem3  5366  csbiota  6540  dffv3  6892  ndmfv  6928  dff3  7111  csbriota  7402  eusvobj2  7422  fnoprabg  7553  zfrep6OLD  7977  dfac5lem5  10219  initoeu1  18201  initoeu1w  18202  initoeu2  18206  termoeu1  18208  termoeu1w  18209  grpidval  18855  0g0  18859  zrninitoringc  20943  txcn  23960  bnj605  35593  bnj607  35602  bnj906  35616  bnj908  35617  neufal  37327  unqsym1  37346  bj-moeub  37894  moxfr  43849  onexomgt  44389  onexoegt  44392  omabs2  44480  eu2ndop1stv  48340  afveu  48368  afv2eu  48453  tz6.12c-afv2  48457  dfatco  48471  initc  50351  thincn0eu  50711  termcterm2  50794  termc2  50798  eufunclem  50801  eufunc  50802  euendfunc  50806  arweuthinc  50809  arweutermc  50810  diag1f1o  50814  diag2f1o  50820  prstchom2ALT  50847  alseuals  51140