Theorem euex 2611

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

Syntax hints:   → wi 4  ∃wex 1806  ∃*wmo 2571  ∃!weu 2602

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 210  df-an 401  df-eu 2603

This theorem is referenced by:  exmoeu  2615  dfeu  2629  euan  2655  euanv  2658  2exeuv  2666  eupickbi  2670  2eu2ex  2677  2exeu  2680  euxfrw  3693  euxfr  3695  zfrep6  5254  eusvnf  5364  eusvnfb  5365  reusv2lem2  5371  reusv2lem3  5372  csbiota  6530  dffv3  6878  ndmfv  6914  dff3  7096  csbriota  7383  eusvobj2  7403  fnoprabg  7534  zfrep6OLD  7952  dfac5lem5  10111  initoeu1  18068  initoeu1w  18069  initoeu2  18073  termoeu1  18075  termoeu1w  18076  grpidval  18719  0g0  18722  zrninitoringc  20761  txcn  23752  bnj605  35240  bnj607  35249  bnj906  35263  bnj908  35264  neufal  36840  unqsym1  36859  bj-moeub  37407  moxfr  43349  onexomgt  43894  onexoegt  43897  omabs2  43985  eu2ndop1stv  47785  afveu  47813  afv2eu  47898  tz6.12c-afv2  47902  dfatco  47916  initc  49788  thincn0eu  50128  termcterm2  50211  termc2  50215  eufunclem  50218  eufunc  50219  euendfunc  50223  arweuthinc  50226  arweutermc  50227  diag1f1o  50231  diag2f1o  50234  prstchom2ALT  50261