Theorem euex 2571

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2532  ∃!weu 2562

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 2563

This theorem is referenced by:  exmoeu  2575  dfeu  2589  euan  2617  euanv  2620  2exeuv  2628  eupickbi  2632  2eu2ex  2639  2exeu  2642  euxfrw  3717  euxfr  3719  eusvnf  5390  eusvnfb  5391  reusv2lem2  5397  reusv2lem3  5398  csbiota  6536  dffv3  6887  tz6.12cOLD  6918  ndmfv  6926  dff3  7101  csbriota  7380  eusvobj2  7400  fnoprabg  7530  zfrep6  7940  dfac5lem5  10121  initoeu1  17960  initoeu1w  17961  initoeu2  17965  termoeu1  17967  termoeu1w  17968  grpidval  18579  0g0  18582  txcn  23129  bnj605  33913  bnj607  33922  bnj906  33936  bnj908  33937  neufal  35286  unqsym1  35305  bj-moeub  35723  moxfr  41420  onexomgt  41980  onexoegt  41983  omabs2  42072  eu2ndop1stv  45823  afveu  45851  afv2eu  45936  tz6.12c-afv2  45940  dfatco  45954  zrninitoringc  46959  thincn0eu  47642  prstchom2ALT  47689