Theorem euex 2578

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

Syntax hints:   → wi 4  ∃wex 1782  ∃*wmo 2539  ∃!weu 2569

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 206  df-an 397  df-eu 2570

This theorem is referenced by:  exmoeu  2582  dfeu  2596  euan  2624  euanv  2627  2exeuv  2635  eupickbi  2639  2eu2ex  2646  2exeu  2649  euxfrw  3657  euxfr  3659  eusvnf  5316  eusvnfb  5317  reusv2lem2  5323  reusv2lem3  5324  csbiota  6430  dffv3  6779  tz6.12c  6808  ndmfv  6813  dff3  6985  csbriota  7257  eusvobj2  7277  fnoprabg  7406  zfrep6  7806  dfac5lem5  9892  initoeu1  17735  initoeu1w  17736  initoeu2  17740  termoeu1  17742  termoeu1w  17743  grpidval  18354  0g0  18357  txcn  22786  bnj605  32896  bnj607  32905  bnj906  32919  bnj908  32920  neufal  34604  unqsym1  34623  bj-moeub  35042  moxfr  40521  eu2ndop1stv  44628  afveu  44656  afv2eu  44741  tz6.12c-afv2  44745  dfatco  44759  zrninitoringc  45640  thincn0eu  46324  prstchom2ALT  46371