Theorem euex 2577

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

Syntax hints:   → wi 4  ∃wex 1781  ∃*wmo 2537  ∃!weu 2568

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 2569

This theorem is referenced by:  exmoeu  2581  dfeu  2595  euan  2621  euanv  2624  2exeuv  2632  eupickbi  2636  2eu2ex  2643  2exeu  2646  euxfrw  3667  euxfr  3669  zfrep6  5224  eusvnf  5334  eusvnfb  5335  reusv2lem2  5341  reusv2lem3  5342  csbiota  6491  dffv3  6836  ndmfv  6872  dff3  7052  csbriota  7339  eusvobj2  7359  fnoprabg  7490  zfrep6OLD  7908  dfac5lem5  10049  initoeu1  17978  initoeu1w  17979  initoeu2  17983  termoeu1  17985  termoeu1w  17986  grpidval  18629  0g0  18632  zrninitoringc  20653  txcn  23591  bnj605  35049  bnj607  35058  bnj906  35072  bnj908  35073  neufal  36588  unqsym1  36607  bj-moeub  37156  moxfr  43124  onexomgt  43669  onexoegt  43672  omabs2  43760  eu2ndop1stv  47573  afveu  47601  afv2eu  47686  tz6.12c-afv2  47690  dfatco  47704  initc  49566  thincn0eu  49906  termcterm2  49989  termc2  49993  eufunclem  49996  eufunc  49997  euendfunc  50001  arweuthinc  50004  arweutermc  50005  diag1f1o  50009  diag2f1o  50012  prstchom2ALT  50039