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 497	1 ⊢ (∃!𝑥𝜑 → ∃𝑥𝜑)

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2538  ∃!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 207  df-an 396  df-eu 2570

This theorem is referenced by:  exmoeu  2582  dfeu  2596  euan  2622  euanv  2625  2exeuv  2633  eupickbi  2637  2eu2ex  2644  2exeu  2647  euxfrw  3680  euxfr  3682  eusvnf  5338  eusvnfb  5339  reusv2lem2  5345  reusv2lem3  5346  csbiota  6486  dffv3  6831  ndmfv  6867  dff3  7047  csbriota  7332  eusvobj2  7352  fnoprabg  7483  zfrep6  7901  dfac5lem5  10041  initoeu1  17939  initoeu1w  17940  initoeu2  17944  termoeu1  17946  termoeu1w  17947  grpidval  18590  0g0  18593  zrninitoringc  20613  txcn  23574  bnj605  35065  bnj607  35074  bnj906  35088  bnj908  35089  neufal  36602  unqsym1  36621  bj-moeub  37052  moxfr  43001  onexomgt  43550  onexoegt  43553  omabs2  43641  eu2ndop1stv  47438  afveu  47466  afv2eu  47551  tz6.12c-afv2  47555  dfatco  47569  initc  49403  thincn0eu  49743  termcterm2  49826  termc2  49830  eufunclem  49833  eufunc  49834  euendfunc  49838  arweuthinc  49841  arweutermc  49842  diag1f1o  49846  diag2f1o  49849  prstchom2ALT  49876