Theorem euex 2607

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

This proof depends on syntax axioms:   → wi 4  ∃wex 1812  ∃*wmo 2567  ∃!weu 2598

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-eu 2599

This theorem is used by:  exmoeu  2611  dfeu  2625  euan  2651  euanv  2654  2exeuv  2662  eupickbi  2666  2eu2ex  2673  2exeu  2676  euxfrw  3686  euxfr  3688  zfrep6  5252  eusvnf  5365  eusvnfb  5366  reusv2lem2  5372  reusv2lem3  5373  csbiota  6533  dffv3  6881  ndmfv  6917  dff3  7099  csbriota  7391  eusvobj2  7411  fnoprabg  7542  zfrep6OLD  7958  dfac5lem5  10127  initoeu1  18094  initoeu1w  18095  initoeu2  18099  termoeu1  18101  termoeu1w  18102  grpidval  18748  0g0  18751  zrninitoringc  20829  txcn  23838  bnj605  35364  bnj607  35373  bnj906  35387  bnj908  35388  neufal  36978  unqsym1  36997  bj-moeub  37545  moxfr  43500  onexomgt  44045  onexoegt  44048  omabs2  44136  eu2ndop1stv  47939  afveu  47967  afv2eu  48052  tz6.12c-afv2  48056  dfatco  48070  initc  49945  thincn0eu  50285  termcterm2  50368  termc2  50372  eufunclem  50375  eufunc  50376  euendfunc  50380  arweuthinc  50383  arweutermc  50384  diag1f1o  50388  diag2f1o  50391  prstchom2ALT  50418  alseuals  50678