Theorem euex 2570

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

Syntax hints:   → wi 4  ∃wex 1779  ∃*wmo 2531  ∃!weu 2561

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 2562

This theorem is referenced by:  exmoeu  2574  dfeu  2588  euan  2614  euanv  2617  2exeuv  2625  eupickbi  2629  2eu2ex  2636  2exeu  2639  euxfrw  3681  euxfr  3683  eusvnf  5331  eusvnfb  5332  reusv2lem2  5338  reusv2lem3  5339  csbiota  6475  dffv3  6818  ndmfv  6855  dff3  7034  csbriota  7321  eusvobj2  7341  fnoprabg  7472  zfrep6  7890  dfac5lem5  10021  initoeu1  17918  initoeu1w  17919  initoeu2  17923  termoeu1  17925  termoeu1w  17926  grpidval  18535  0g0  18538  zrninitoringc  20561  txcn  23511  bnj605  34880  bnj607  34889  bnj906  34903  bnj908  34904  neufal  36390  unqsym1  36409  bj-moeub  36833  moxfr  42675  onexomgt  43224  onexoegt  43227  omabs2  43315  eu2ndop1stv  47119  afveu  47147  afv2eu  47232  tz6.12c-afv2  47236  dfatco  47250  initc  49086  thincn0eu  49426  termcterm2  49509  termc2  49513  eufunclem  49516  eufunc  49517  euendfunc  49521  arweuthinc  49524  arweutermc  49525  diag1f1o  49529  diag2f1o  49532  prstchom2ALT  49559