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  3681  euxfr  3683  zfrep6  5238  eusvnf  5341  eusvnfb  5342  reusv2lem2  5348  reusv2lem3  5349  csbiota  6495  dffv3  6840  ndmfv  6876  dff3  7056  csbriota  7342  eusvobj2  7362  fnoprabg  7493  zfrep6OLD  7911  dfac5lem5  10051  initoeu1  17949  initoeu1w  17950  initoeu2  17954  termoeu1  17956  termoeu1w  17957  grpidval  18600  0g0  18603  zrninitoringc  20626  txcn  23587  bnj605  35089  bnj607  35098  bnj906  35112  bnj908  35113  neufal  36628  unqsym1  36647  bj-moeub  37124  moxfr  43078  onexomgt  43627  onexoegt  43630  omabs2  43718  eu2ndop1stv  47514  afveu  47542  afv2eu  47627  tz6.12c-afv2  47631  dfatco  47645  initc  49479  thincn0eu  49819  termcterm2  49902  termc2  49906  eufunclem  49909  eufunc  49910  euendfunc  49914  arweuthinc  49917  arweutermc  49918  diag1f1o  49922  diag2f1o  49925  prstchom2ALT  49952