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 501	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

This proof depends on syntax axioms:   → wi 4  ∃wex 1809  ∃*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 401  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  3684  euxfr  3686  zfrep6  5250  eusvnf  5363  eusvnfb  5364  reusv2lem2  5370  reusv2lem3  5371  csbiota  6529  dffv3  6877  ndmfv  6913  dff3  7095  csbriota  7382  eusvobj2  7402  fnoprabg  7533  zfrep6OLD  7948  dfac5lem5  10116  initoeu1  18072  initoeu1w  18073  initoeu2  18077  termoeu1  18079  termoeu1w  18080  grpidval  18723  0g0  18726  zrninitoringc  20784  txcn  23792  bnj605  35304  bnj607  35313  bnj906  35327  bnj908  35328  neufal  36945  unqsym1  36964  bj-moeub  37512  moxfr  43451  onexomgt  43996  onexoegt  43999  omabs2  44087  eu2ndop1stv  47890  afveu  47918  afv2eu  48003  tz6.12c-afv2  48007  dfatco  48021  initc  49897  thincn0eu  50237  termcterm2  50320  termc2  50324  eufunclem  50327  eufunc  50328  euendfunc  50332  arweuthinc  50335  arweutermc  50336  diag1f1o  50340  diag2f1o  50343  prstchom2ALT  50370  alseuals  50630