Theorem euex 2570

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2531  ∃!weu 2561

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

This theorem is referenced by:  exmoeu  2574  dfeu  2588  euan  2614  euanv  2617  2exeuv  2625  eupickbi  2629  2eu2ex  2636  2exeu  2639  euxfrw  3692  euxfr  3694  eusvnf  5347  eusvnfb  5348  reusv2lem2  5354  reusv2lem3  5355  csbiota  6504  dffv3  6854  tz6.12cOLD  6885  ndmfv  6893  dff3  7072  csbriota  7359  eusvobj2  7379  fnoprabg  7512  zfrep6  7933  dfac5lem5  10080  initoeu1  17973  initoeu1w  17974  initoeu2  17978  termoeu1  17980  termoeu1w  17981  grpidval  18588  0g0  18591  zrninitoringc  20585  txcn  23513  bnj605  34897  bnj607  34906  bnj906  34920  bnj908  34921  neufal  36394  unqsym1  36413  bj-moeub  36837  moxfr  42680  onexomgt  43230  onexoegt  43233  omabs2  43321  eu2ndop1stv  47126  afveu  47154  afv2eu  47239  tz6.12c-afv2  47243  dfatco  47257  initc  49080  thincn0eu  49420  termcterm2  49503  termc2  49507  eufunclem  49510  eufunc  49511  euendfunc  49515  arweuthinc  49518  arweutermc  49519  diag1f1o  49523  diag2f1o  49526  prstchom2ALT  49553