Theorem euex 2575

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

Syntax hints:   → wi 4  ∃wex 1776  ∃*wmo 2536  ∃!weu 2566

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 2567

This theorem is referenced by:  exmoeu  2579  dfeu  2593  euan  2619  euanv  2622  2exeuv  2630  eupickbi  2634  2eu2ex  2641  2exeu  2644  euxfrw  3730  euxfr  3732  eusvnf  5398  eusvnfb  5399  reusv2lem2  5405  reusv2lem3  5406  csbiota  6556  dffv3  6903  tz6.12cOLD  6934  ndmfv  6942  dff3  7120  csbriota  7403  eusvobj2  7423  fnoprabg  7556  zfrep6  7978  dfac5lem5  10165  initoeu1  18065  initoeu1w  18066  initoeu2  18070  termoeu1  18072  termoeu1w  18073  grpidval  18687  0g0  18690  zrninitoringc  20693  txcn  23650  bnj605  34900  bnj607  34909  bnj906  34923  bnj908  34924  neufal  36389  unqsym1  36408  bj-moeub  36832  moxfr  42680  onexomgt  43230  onexoegt  43233  omabs2  43322  eu2ndop1stv  47075  afveu  47103  afv2eu  47188  tz6.12c-afv2  47192  dfatco  47206  thincn0eu  48832  prstchom2ALT  48880