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  3689  euxfr  3691  eusvnf  5342  eusvnfb  5343  reusv2lem2  5349  reusv2lem3  5350  csbiota  6492  dffv3  6836  tz6.12cOLD  6867  ndmfv  6875  dff3  7054  csbriota  7341  eusvobj2  7361  fnoprabg  7492  zfrep6  7913  dfac5lem5  10056  initoeu1  17953  initoeu1w  17954  initoeu2  17958  termoeu1  17960  termoeu1w  17961  grpidval  18570  0g0  18573  zrninitoringc  20596  txcn  23546  bnj605  34890  bnj607  34899  bnj906  34913  bnj908  34914  neufal  36387  unqsym1  36406  bj-moeub  36830  moxfr  42673  onexomgt  43223  onexoegt  43226  omabs2  43314  eu2ndop1stv  47119  afveu  47147  afv2eu  47232  tz6.12c-afv2  47236  dfatco  47250  initc  49073  thincn0eu  49413  termcterm2  49496  termc2  49500  eufunclem  49503  eufunc  49504  euendfunc  49508  arweuthinc  49511  arweutermc  49512  diag1f1o  49516  diag2f1o  49519  prstchom2ALT  49546