Theorem euex 2576

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

Syntax hints:   → wi 4  ∃wex 1787  ∃*wmo 2537  ∃!weu 2567

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 210  df-an 400  df-eu 2568

This theorem is referenced by:  exmoeu  2580  dfeu  2594  euan  2622  euanv  2625  2exeuv  2633  eupickbi  2637  2eu2ex  2644  2exeu  2647  euxfrw  3634  euxfr  3636  eusvnf  5285  eusvnfb  5286  reusv2lem2  5292  reusv2lem3  5293  csbiota  6373  dffv3  6713  tz6.12c  6742  ndmfv  6747  dff3  6919  csbriota  7186  eusvobj2  7206  fnoprabg  7333  zfrep6  7728  dfac5lem5  9741  initoeu1  17517  initoeu1w  17518  initoeu2  17522  termoeu1  17524  termoeu1w  17525  grpidval  18133  0g0  18136  txcn  22523  bnj605  32600  bnj607  32609  bnj906  32623  bnj908  32624  neufal  34332  unqsym1  34351  bj-moeub  34770  moxfr  40217  eu2ndop1stv  44289  afveu  44317  afv2eu  44402  tz6.12c-afv2  44406  dfatco  44420  zrninitoringc  45302  thincn0eu  45986  prstchom2ALT  46031