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 496	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  3668  euxfr  3670  zfrep6  5225  eusvnf  5331  eusvnfb  5332  reusv2lem2  5338  reusv2lem3  5339  csbiota  6487  dffv3  6832  ndmfv  6868  dff3  7048  csbriota  7334  eusvobj2  7354  fnoprabg  7485  zfrep6OLD  7903  dfac5lem5  10044  initoeu1  17973  initoeu1w  17974  initoeu2  17978  termoeu1  17980  termoeu1w  17981  grpidval  18624  0g0  18627  zrninitoringc  20648  txcn  23605  bnj605  35069  bnj607  35078  bnj906  35092  bnj908  35093  neufal  36608  unqsym1  36627  bj-moeub  37176  moxfr  43142  onexomgt  43691  onexoegt  43694  omabs2  43782  eu2ndop1stv  47589  afveu  47617  afv2eu  47702  tz6.12c-afv2  47706  dfatco  47720  initc  49582  thincn0eu  49922  termcterm2  50005  termc2  50009  eufunclem  50012  eufunc  50013  euendfunc  50017  arweuthinc  50020  arweutermc  50021  diag1f1o  50025  diag2f1o  50028  prstchom2ALT  50055