Theorem euex 2575

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

Syntax hints:   → wi 4  ∃wex 1780  ∃*wmo 2535  ∃!weu 2566

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 2567

This theorem is referenced by:  exmoeu  2579  dfeu  2593  euan  2619  euanv  2622  2exeuv  2630  eupickbi  2634  2eu2ex  2641  2exeu  2644  euxfrw  3677  euxfr  3679  eusvnf  5335  eusvnfb  5336  reusv2lem2  5342  reusv2lem3  5343  csbiota  6483  dffv3  6828  ndmfv  6864  dff3  7043  csbriota  7328  eusvobj2  7348  fnoprabg  7479  zfrep6  7897  dfac5lem5  10035  initoeu1  17933  initoeu1w  17934  initoeu2  17938  termoeu1  17940  termoeu1w  17941  grpidval  18584  0g0  18587  zrninitoringc  20607  txcn  23568  bnj605  35012  bnj607  35021  bnj906  35035  bnj908  35036  neufal  36549  unqsym1  36568  bj-moeub  36993  moxfr  42876  onexomgt  43425  onexoegt  43428  omabs2  43516  eu2ndop1stv  47313  afveu  47341  afv2eu  47426  tz6.12c-afv2  47430  dfatco  47444  initc  49278  thincn0eu  49618  termcterm2  49701  termc2  49705  eufunclem  49708  eufunc  49709  euendfunc  49713  arweuthinc  49716  arweutermc  49717  diag1f1o  49721  diag2f1o  49724  prstchom2ALT  49751